diff options
Diffstat (limited to 'test/regress/regress0/arith')
32 files changed, 176 insertions, 147 deletions
diff --git a/test/regress/regress0/arith/arith.01.cvc b/test/regress/regress0/arith/arith.01.cvc deleted file mode 100644 index 08d591590..000000000 --- a/test/regress/regress0/arith/arith.01.cvc +++ /dev/null @@ -1,5 +0,0 @@ -% EXPECT: entailed -x : REAL; -y : REAL; - -QUERY (x * y ) = (y * x); diff --git a/test/regress/regress0/arith/arith.01.cvc.smt2 b/test/regress/regress0/arith/arith.01.cvc.smt2 new file mode 100644 index 000000000..eac4fe1b8 --- /dev/null +++ b/test/regress/regress0/arith/arith.01.cvc.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () Real) +(declare-fun y () Real) +(check-sat-assuming ( (not (= (* x y) (* y x))) )) diff --git a/test/regress/regress0/arith/arith.02.cvc b/test/regress/regress0/arith/arith.02.cvc deleted file mode 100644 index e0a48c357..000000000 --- a/test/regress/regress0/arith/arith.02.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% EXPECT: entailed -x : REAL; -y : REAL; -z : REAL; - -QUERY x*(y*z) = (x*y)*z; diff --git a/test/regress/regress0/arith/arith.02.cvc.smt2 b/test/regress/regress0/arith/arith.02.cvc.smt2 new file mode 100644 index 000000000..5c44e1bec --- /dev/null +++ b/test/regress/regress0/arith/arith.02.cvc.smt2 @@ -0,0 +1,7 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun z () Real) +(check-sat-assuming ( (not (= (* x (* y z)) (* (* x y) z))) )) diff --git a/test/regress/regress0/arith/arith.03.cvc b/test/regress/regress0/arith/arith.03.cvc deleted file mode 100644 index ce54c8b7e..000000000 --- a/test/regress/regress0/arith/arith.03.cvc +++ /dev/null @@ -1,5 +0,0 @@ -% EXPECT: entailed -x : REAL; -y : REAL; - -QUERY (x + y)*(x + y) = x*x + 2*x*y + y*y; diff --git a/test/regress/regress0/arith/arith.03.cvc.smt2 b/test/regress/regress0/arith/arith.03.cvc.smt2 new file mode 100644 index 000000000..777526117 --- /dev/null +++ b/test/regress/regress0/arith/arith.03.cvc.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () Real) +(declare-fun y () Real) +(check-sat-assuming ( (not (let ((_let_1 (+ x y))) (= (* _let_1 _let_1) (+ (+ (* x x) (* (* 2 x) y)) (* y y))))) )) diff --git a/test/regress/regress0/arith/bug549.cvc b/test/regress/regress0/arith/bug549.cvc deleted file mode 100644 index bfb3e75d5..000000000 --- a/test/regress/regress0/arith/bug549.cvc +++ /dev/null @@ -1,3 +0,0 @@ -% EXPECT: entailed -a, b : REAL; -QUERY (a*b)^5 = b*a*a*a*a*b*b*b*b*a; diff --git a/test/regress/regress0/arith/bug549.cvc.smt2 b/test/regress/regress0/arith/bug549.cvc.smt2 new file mode 100644 index 000000000..74bdc8878 --- /dev/null +++ b/test/regress/regress0/arith/bug549.cvc.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun a () Real) +(declare-fun b () Real) +(check-sat-assuming ( (not (= (^ (* a b) 5) (* (* (* (* (* (* (* (* (* b a) a) a) a) b) b) b) b) a))) )) diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc deleted file mode 100644 index 84954a3ea..000000000 --- a/test/regress/regress0/arith/integers/arith-int-014.cvc +++ /dev/null @@ -1,5 +0,0 @@ -% EXPECT: not_entailed -x0, x1, x2, x3 : INT; -ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ; -ASSERT (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-014.cvc.smt2 new file mode 100644 index 000000000..02aa0d5b1 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-014.cvc.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(assert (<= (+ (+ (+ (* 10 x0) (* 25 x1)) (* 10 x2)) (* (- 28) x3)) 20)) +(assert (<= (+ (+ (+ (* 24 x0) (* (- 9) x1)) (* (- 12) x2)) (* 15 x3)) 3)) +(check-sat) diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc deleted file mode 100644 index 8f8b01fc9..000000000 --- a/test/regress/regress0/arith/integers/arith-int-015.cvc +++ /dev/null @@ -1,5 +0,0 @@ -% EXPECT: not_entailed -x0, x1, x2, x3 : INT; -ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ; -ASSERT (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-015.cvc.smt2 new file mode 100644 index 000000000..5fecc9da0 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-015.cvc.smt2 @@ -0,0 +1,10 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(assert (> (+ (+ (+ (* (- 22) x0) (* (- 3) x1)) (* 9 x2)) (* (- 13) x3)) (- 31))) +(assert (> (+ (+ (+ (* 31 x0) (* (- 17) x1)) (* 28 x2)) (* (- 16) x3)) (- 28))) +(check-sat) diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc deleted file mode 100644 index 66f02401b..000000000 --- a/test/regress/regress0/arith/integers/arith-int-021.cvc +++ /dev/null @@ -1,4 +0,0 @@ -% EXPECT: not_entailed -x0, x1, x2, x3 : INT; -ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-021.cvc.smt2 new file mode 100644 index 000000000..c7c20c65e --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-021.cvc.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(assert (< (+ (+ (+ (* 8 x0) (* (- 27) x1)) (* 29 x2)) (* (- 13) x3)) 12)) +(check-sat) diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc deleted file mode 100644 index b3d79e8ff..000000000 --- a/test/regress/regress0/arith/integers/arith-int-023.cvc +++ /dev/null @@ -1,4 +0,0 @@ -% EXPECT: not_entailed -x0, x1, x2, x3 : INT; -ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-023.cvc.smt2 new file mode 100644 index 000000000..5bf51fcc7 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-023.cvc.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(assert (<= (+ (+ (+ (* 29 x0) (* (- 19) x1)) (* 23 x2)) (* 15 x3)) 9)) +(check-sat) diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc deleted file mode 100644 index e905da9a0..000000000 --- a/test/regress/regress0/arith/integers/arith-int-025.cvc +++ /dev/null @@ -1,4 +0,0 @@ -% EXPECT: not_entailed -x0, x1, x2, x3 : INT; -ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-025.cvc.smt2 new file mode 100644 index 000000000..625b5d82d --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-025.cvc.smt2 @@ -0,0 +1,9 @@ +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(assert (>= (+ (+ (+ (* (- 19) x0) (* (- 29) x1)) (* 2 x2)) (* 26 x3)) 3)) +(check-sat) diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc deleted file mode 100644 index b6db26e86..000000000 --- a/test/regress/regress0/arith/integers/arith-int-042.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: entailed -x0, x1, x2, x3 : INT; -ASSERT (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ; -ASSERT (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ; -ASSERT (19 * x0) + (25 * x1) + (-32 * x2) + (-29 * x3) <= 14 ; -ASSERT (6 * x0) + (22 * x1) + (-24 * x2) + (-6 * x3) < -21 ; -ASSERT (-18 * x0) + (-21 * x1) + (-29 * x2) + (12 * x3) > 17 ; -ASSERT (-25 * x0) + (-5 * x1) + (-22 * x2) + (-7 * x3) > -21; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-042.cvc.smt2 new file mode 100644 index 000000000..bbe6d209e --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-042.cvc.smt2 @@ -0,0 +1,14 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(assert (= (+ (+ (+ (* (- 9) x0) (* 25 x1)) (* 0 x2)) (* 13 x3)) 17)) +(assert (= (+ (+ (+ (* (- 6) x0) (* 32 x1)) (* 2 x2)) (* (- 32) x3)) (- 5))) +(assert (<= (+ (+ (+ (* 19 x0) (* 25 x1)) (* (- 32) x2)) (* (- 29) x3)) 14)) +(assert (< (+ (+ (+ (* 6 x0) (* 22 x1)) (* (- 24) x2)) (* (- 6) x3)) (- 21))) +(assert (> (+ (+ (+ (* (- 18) x0) (* (- 21) x1)) (* (- 29) x2)) (* 12 x3)) 17)) +(assert (> (+ (+ (+ (* (- 25) x0) (* (- 5) x1)) (* (- 22) x2)) (* (- 7) x3)) (- 21))) +(check-sat) diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc deleted file mode 100644 index 3fd20a0b6..000000000 --- a/test/regress/regress0/arith/integers/arith-int-042.min.cvc +++ /dev/null @@ -1,4 +0,0 @@ -% EXPECT: entailed -x1: INT; -x0: INT; -QUERY NOT (((x0 * 6) + (x1 * 32)) = 1); diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-042.min.cvc.smt2 new file mode 100644 index 000000000..62acf2e70 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc.smt2 @@ -0,0 +1,6 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x1 () Int) +(declare-fun x0 () Int) +(check-sat-assuming ( (= (+ (* x0 6) (* x1 32)) 1) )) diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc deleted file mode 100644 index 1739b3364..000000000 --- a/test/regress/regress0/arith/integers/arith-int-079.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: entailed -x0, x1, x2, x3 : INT; -ASSERT (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ; -ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ; -ASSERT (8 * x0) + (25 * x1) + (-7 * x2) + (-29 * x3) < -25 ; -ASSERT (27 * x0) + (17 * x1) + (-24 * x2) + (-5 * x3) <= 13 ; -ASSERT (5 * x0) + (-3 * x1) + (0 * x2) + (4 * x3) < -26 ; -ASSERT (25 * x0) + (7 * x1) + (27 * x2) + (-14 * x3) < 30 ; -ASSERT (-22 * x0) + (-17 * x1) + (9 * x2) + (-20 * x3) < -19 ; -ASSERT (31 * x0) + (-16 * x1) + (0 * x2) + (6 * x3) >= 18; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc.smt2 b/test/regress/regress0/arith/integers/arith-int-079.cvc.smt2 new file mode 100644 index 000000000..16c8c7ea4 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-079.cvc.smt2 @@ -0,0 +1,16 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(assert (= (+ (+ (+ (* 6 x0) (* 2 x1)) (* 22 x2)) (* (- 18) x3)) (- 15))) +(assert (let ((_let_1 (- 25))) (> (+ (+ (+ (* (- 8) x0) (* _let_1 x1)) (* _let_1 x2)) (* 7 x3)) 10))) +(assert (< (+ (+ (+ (* 8 x0) (* 25 x1)) (* (- 7) x2)) (* (- 29) x3)) (- 25))) +(assert (<= (+ (+ (+ (* 27 x0) (* 17 x1)) (* (- 24) x2)) (* (- 5) x3)) 13)) +(assert (< (+ (+ (+ (* 5 x0) (* (- 3) x1)) (* 0 x2)) (* 4 x3)) (- 26))) +(assert (< (+ (+ (+ (* 25 x0) (* 7 x1)) (* 27 x2)) (* (- 14) x3)) 30)) +(assert (< (+ (+ (+ (* (- 22) x0) (* (- 17) x1)) (* 9 x2)) (* (- 20) x3)) (- 19))) +(assert (>= (+ (+ (+ (* 31 x0) (* (- 16) x1)) (* 0 x2)) (* 6 x3)) 18)) +(check-sat) diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc deleted file mode 100644 index ed6cb747e..000000000 --- a/test/regress/regress0/arith/integers/arith-interval.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% EXPECT: entailed -x: INT; -P: INT -> BOOLEAN; - -ASSERT 1 <= x AND x <= 2; -ASSERT P(1) AND P(2); -QUERY P(x); diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc.smt2 b/test/regress/regress0/arith/integers/arith-interval.cvc.smt2 new file mode 100644 index 000000000..1a0fcd737 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-interval.cvc.smt2 @@ -0,0 +1,8 @@ +; EXPECT: unsat +(set-logic ALL) +(set-option :incremental false) +(declare-fun x () Int) +(declare-fun P (Int) Bool) +(assert (and (<= 1 x) (<= x 2))) +(assert (and (P 1) (P 2))) +(check-sat-assuming ( (not (P x)) )) diff --git a/test/regress/regress0/arith/miplib.cvc b/test/regress/regress0/arith/miplib.cvc deleted file mode 100644 index a7ae19b0a..000000000 --- a/test/regress/regress0/arith/miplib.cvc +++ /dev/null @@ -1,28 +0,0 @@ -% COMMAND-LINE: --miplib-trick -% EXPECT: sat - -tmp1, tmp2, tmp3 : INT; -x, y, z : BOOLEAN; - -% x = {0, 1}, (NOT x) = 1 - x -% i*Nx + j*Ny + k = 0 -% i*x + j*Ny + k = 4 -% i*Nx + j*y + k = 6 -% i*x + j*y + k = 10 - -ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0; -ASSERT x AND (NOT y AND TRUE) => tmp1 = 4; -ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6; -ASSERT x AND ( y AND TRUE) => tmp1 = 10; - -ASSERT NOT x AND (NOT z AND TRUE) => tmp2 = 0; -ASSERT x AND (NOT z AND TRUE) => tmp2 = 2; -ASSERT NOT x AND ( z AND TRUE) => tmp2 = 9; -ASSERT x AND ( z AND TRUE) => tmp2 = 11; - -ASSERT NOT y AND (NOT z AND TRUE) => tmp3 = 0; -ASSERT y AND (NOT z AND TRUE) => tmp3 = 5; -ASSERT NOT y AND ( z AND TRUE) => tmp3 = 16; -ASSERT y AND ( z AND TRUE) => tmp3 = 21; - -CHECKSAT; diff --git a/test/regress/regress0/arith/miplib.cvc.smt2 b/test/regress/regress0/arith/miplib.cvc.smt2 new file mode 100644 index 000000000..3b31b4f1b --- /dev/null +++ b/test/regress/regress0/arith/miplib.cvc.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --miplib-trick +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun tmp1 () Int) +(declare-fun tmp2 () Int) +(declare-fun tmp3 () Int) +(declare-fun x () Bool) +(declare-fun y () Bool) +(declare-fun z () Bool) +(assert (=> (and (not x) (and (not y) true)) (= tmp1 0))) +(assert (=> (and x (and (not y) true)) (= tmp1 4))) +(assert (=> (and (not x) (and y true)) (= tmp1 6))) +(assert (=> (and x (and y true)) (= tmp1 10))) +(assert (=> (and (not x) (and (not z) true)) (= tmp2 0))) +(assert (=> (and x (and (not z) true)) (= tmp2 2))) +(assert (=> (and (not x) (and z true)) (= tmp2 9))) +(assert (=> (and x (and z true)) (= tmp2 11))) +(assert (=> (and (not y) (and (not z) true)) (= tmp3 0))) +(assert (=> (and y (and (not z) true)) (= tmp3 5))) +(assert (=> (and (not y) (and z true)) (= tmp3 16))) +(assert (=> (and y (and z true)) (= tmp3 21))) +(check-sat) diff --git a/test/regress/regress0/arith/miplib2.cvc b/test/regress/regress0/arith/miplib2.cvc deleted file mode 100644 index ce2e9712e..000000000 --- a/test/regress/regress0/arith/miplib2.cvc +++ /dev/null @@ -1,32 +0,0 @@ -% COMMAND-LINE: --miplib-trick -% EXPECT: sat - -tmp1, tmp2, tmp3 : INT; -x, y, z : BOOLEAN; - -% x = {0, 1}, (NOT x) = 1 - x -% i*Nx + j*Ny + k = 0 -% i*x + j*Ny + k = 4 -% i*Nx + j*y + k = 6 -% i*x + j*y + k = 10 - -ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0; -ASSERT x AND (NOT y AND TRUE) => tmp1 = 4; -ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6; -ASSERT x AND ( y AND TRUE) => tmp1 = 10; - -ASSERT NOT x AND (NOT z AND TRUE) => tmp2 = 0; -ASSERT x AND (NOT z AND TRUE) => tmp2 = 2; -ASSERT NOT x AND ( z AND TRUE) => tmp2 = 9; -ASSERT x AND ( z AND TRUE) => tmp2 = 11; - -ASSERT NOT y AND (NOT z AND TRUE) => tmp3 = 0; -ASSERT y AND (NOT z AND TRUE) => tmp3 = 5; -ASSERT NOT y AND ( z AND TRUE) => tmp3 = 16; -ASSERT y AND ( z AND TRUE) => tmp3 = 21; - -% miplib trick does not apply to blocks 1 and 2, x occurs outside -% of the tmp definitions -ASSERT x; - -CHECKSAT; diff --git a/test/regress/regress0/arith/miplib2.cvc.smt2 b/test/regress/regress0/arith/miplib2.cvc.smt2 new file mode 100644 index 000000000..e95385bb1 --- /dev/null +++ b/test/regress/regress0/arith/miplib2.cvc.smt2 @@ -0,0 +1,24 @@ +; COMMAND-LINE: --miplib-trick +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun tmp1 () Int) +(declare-fun tmp2 () Int) +(declare-fun tmp3 () Int) +(declare-fun x () Bool) +(declare-fun y () Bool) +(declare-fun z () Bool) +(assert (=> (and (not x) (and (not y) true)) (= tmp1 0))) +(assert (=> (and x (and (not y) true)) (= tmp1 4))) +(assert (=> (and (not x) (and y true)) (= tmp1 6))) +(assert (=> (and x (and y true)) (= tmp1 10))) +(assert (=> (and (not x) (and (not z) true)) (= tmp2 0))) +(assert (=> (and x (and (not z) true)) (= tmp2 2))) +(assert (=> (and (not x) (and z true)) (= tmp2 9))) +(assert (=> (and x (and z true)) (= tmp2 11))) +(assert (=> (and (not y) (and (not z) true)) (= tmp3 0))) +(assert (=> (and y (and (not z) true)) (= tmp3 5))) +(assert (=> (and (not y) (and z true)) (= tmp3 16))) +(assert (=> (and y (and z true)) (= tmp3 21))) +(assert x) +(check-sat) diff --git a/test/regress/regress0/arith/miplib4.cvc b/test/regress/regress0/arith/miplib4.cvc deleted file mode 100644 index 722122b38..000000000 --- a/test/regress/regress0/arith/miplib4.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% COMMAND-LINE: --miplib-trick -% EXPECT: sat - -tmp1 : INT; -x, y : BOOLEAN; - -% nonlinear combination, not eligible for miplib trick replacement -ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0; -ASSERT x AND (NOT y AND TRUE) => tmp1 = 4; -ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6; -ASSERT x AND ( y AND TRUE) => tmp1 = 12; - -ASSERT tmp1 > 10; - -CHECKSAT; diff --git a/test/regress/regress0/arith/miplib4.cvc.smt2 b/test/regress/regress0/arith/miplib4.cvc.smt2 new file mode 100644 index 000000000..d669133d1 --- /dev/null +++ b/test/regress/regress0/arith/miplib4.cvc.smt2 @@ -0,0 +1,13 @@ +; COMMAND-LINE: --miplib-trick +; EXPECT: sat +(set-logic ALL) +(set-option :incremental false) +(declare-fun tmp1 () Int) +(declare-fun x () Bool) +(declare-fun y () Bool) +(assert (=> (and (not x) (and (not y) true)) (= tmp1 0))) +(assert (=> (and x (and (not y) true)) (= tmp1 4))) +(assert (=> (and (not x) (and y true)) (= tmp1 6))) +(assert (=> (and x (and y true)) (= tmp1 12))) +(assert (> tmp1 10)) +(check-sat) |