Commit 5e8e081e authored by Andrei Paskevich's avatar Andrei Paskevich

there is no unary minus in Yices 1.0

parent 560952e5
......@@ -42,7 +42,7 @@ theory int.Int
syntax function (+) "(+ %1 %2)"
syntax function (-) "(- %1 %2)"
syntax function (*) "(* %1 %2)"
syntax function (-_) "(- %1)"
syntax function (-_) "(- 0 %1)"
syntax predicate (<=) "(<= %1 %2)"
syntax predicate (<) "(< %1 %2)"
......@@ -81,7 +81,7 @@ theory real.Real
(* 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 (-_) "(- 0 %1)"
(* syntax function inv "(/ 1 %1)" *)
syntax predicate (<=) "(<= %1 %2)"
......
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