diff --git a/drivers/cvc4.drv b/drivers/cvc4.drv index 21ccbca26d1507b82c78229d719c5c0ae27f2c2a..538bf7f4634a82b0cb3319696ae9f13cc20da31b 100644 --- a/drivers/cvc4.drv +++ b/drivers/cvc4.drv @@ -1,9 +1,2 @@ import "cvc4_bare.drv" import "discrimination.gen" - -(* -Local Variables: -mode: why -compile-command: "unset LANG; make -C .. bench" -End: -*) diff --git a/drivers/cvc4_bare.drv b/drivers/cvc4_bare.drv index 432a7167698ac6b7086ba29db8768b3eefcd48c0..c372adf08f56abb977615d2632b5455ea6fb88dc 100644 --- a/drivers/cvc4_bare.drv +++ b/drivers/cvc4_bare.drv @@ -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: -*) diff --git a/drivers/smt-libv2.drv b/drivers/smt-libv2.drv index 024c12c6a00c83d71865214813fbf190e1a7924d..594f2a78a3edf2b8dad53dea70bfba06760ad2e0 100644 --- a/drivers/smt-libv2.drv +++ b/drivers/smt-libv2.drv @@ -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: -*) diff --git a/drivers/z3.drv b/drivers/z3.drv index 60d01662ee1d733d7e42bd634953e4975dd4d5e8..cb771b71eff313e750ef383b35a266d26a1e52ee 100644 --- a/drivers/z3.drv +++ b/drivers/z3.drv @@ -1,9 +1,2 @@ import "z3_bare.drv" import "discrimination.gen" - -(* -Local Variables: -mode: why -compile-command: "unset LANG; make -C .. bench" -End: -*) diff --git a/drivers/z3_bare.drv b/drivers/z3_bare.drv index de397aa9115329772e832a2bd176e09bf0f8fa3f..5de0de7344c63b7d4f716b7bd7f091f596e4c93f 100644 --- a/drivers/z3_bare.drv +++ b/drivers/z3_bare.drv @@ -1,3 +1,10 @@ +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: -*)