Commit 996a6be6 authored by MARCHE Claude's avatar MARCHE Claude

CVC4 1.4: use axiomatic version of div and mod instead of built-in ones

This should restore the current failing replay of nightly bench
parent 34e16135
......@@ -48,20 +48,11 @@ steplimitexceeded "??"
(** 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)"
remove prop Mod_bound
remove prop Div_mod
remove prop Mod_1
remove prop Div_1
end
(*
theory int.ComputerDivision
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
syntax function mod "(mod %1 %2)"
remove prop Mod_bound
......
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