Commit fbb0fd38 authored by Francois Bobot's avatar Francois Bobot
Browse files

Z3 knows EuclidieanDivision

parent 8420e950
......@@ -63,6 +63,14 @@ theory int.Int
end
theory int.EuclideanDivision
syntax logic div "(div %1 %2)"
syntax logic mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
theory transform.encoding_decorate.Kept
tag cloned type t "encoding_decorate : kept"
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment