Commit 293b3b5a authored by MARCHE Claude's avatar MARCHE Claude

Removed the experimental use of built-in division of CVC4 and veriT,

since results are better with the Why3 axiomatic version
parent 427639cb
......@@ -32,8 +32,8 @@ timeout "interrupted by timeout"
(** Extra theories supported by CVC4 *)
(* Disabled:
CVC4 division seems to be neither the Euclidean one, nor the Computer one
*)
CVC4 seems less efficient with its built-in implementation than
with the axiomatic version
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -42,14 +42,4 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
(*
theory int.ComputerDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
*)
......@@ -29,6 +29,8 @@ transformation "simplify_formula"
transformation "encoding_smt"
transformation "encoding_sort"
(*
disabled: veriT seems more efficient with the axiomatic version
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
......@@ -37,7 +39,7 @@ theory int.EuclideanDivision
remove prop Mod_1
remove prop Div_1
end
*)
(*
Local Variables:
......
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