Commit d49abbed authored by François Bobot's avatar François Bobot

remove builtin (/) in yices

Fix the warning in 8e207729
Add a check for yices on real in nightly-build
parent 2165340a
......@@ -77,9 +77,11 @@ theory real.Real
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (/) "(/ %1 %2)"
(* Yices division doesn't accept anything else than constant on
denominator so we don't use it (except for constant cf printer) *)
(* syntax function (/) "(/ %1 %2)" *)
syntax function (-_) "(- %1)"
syntax function inv "(/ 1 %1)"
(* syntax function inv "(/ 1 %1)" *)
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
......
......@@ -13,6 +13,9 @@
<proof prover="z3" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="yices" timelimit="10" edited="" obsolete="false">
<result status="valid" time="0.00"/>
</proof>
<proof prover="spass" timelimit="10" edited="" obsolete="false">
<result status="timeout" time="10.07"/>
</proof>
......
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