Commit 8600e65a authored by Andrei Paskevich's avatar Andrei Paskevich

z3_bare.drv: re-add "(set-logic AUFNIRA)" to the prelude

parent 700f4deb
import "cvc4_bare.drv"
import "discrimination.gen"
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
......@@ -8,8 +8,7 @@ prelude "(set-logic AUFNIRA)" (* how come bv is supported by cvc4 in this logi
import "smt-libv2.drv"
(* CVC4 division seems to be neither the Euclidean one,
nor the Computer one *)
(* CVC4 division seems to be neither the Euclidean one, nor the Computer one *)
(*
theory int.EuclideanDivision
syntax function div "(div %1 %2)"
......@@ -29,10 +28,3 @@ theory int.ComputerDivision
remove prop Div_1
end
*)
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
......@@ -468,10 +468,3 @@ theory bv.BVConverter_8_16
remove prop back_from_bigBV
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
import "z3_bare.drv"
import "discrimination.gen"
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
prelude "(set-logic AUFNIRA)"
(** A : Array
UF : Uninterpreted Function
DT : Datatypes (not needed at the end ...)
NIRA : NonLinear Integer Reals Arithmetic
*)
import "smt-libv2.drv"
(* div/mod of Z3 seems to be Euclidean Division *)
......@@ -19,10 +26,3 @@ theory real.FromInt
remove prop Mul
remove prop Neg
end
(*
Local Variables:
mode: why
compile-command: "unset LANG; make -C .. bench"
End:
*)
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