diff options
Diffstat (limited to 'test/regress/regress1')
113 files changed, 241 insertions, 200 deletions
diff --git a/test/regress/regress1/arith/arith-brab-test.smt2 b/test/regress/regress1/arith/arith-brab-test.smt2 new file mode 100644 index 000000000..7856ae0e6 --- /dev/null +++ b/test/regress/regress1/arith/arith-brab-test.smt2 @@ -0,0 +1,23 @@ +; COMMAND-LINE: --arith-brab +; COMMAND-LINE: --no-arith-brab +; EXPECT: sat +(set-logic ALL) + +(declare-fun x1 () Real) +(declare-fun y1 () Real) +(declare-fun m1 () Real) +(declare-fun b1 () Real) + +(declare-fun x () Int) +(declare-fun y () Int) + +(assert (= y1 (+ b1 (* m1 x1)))) +(assert (= x1 (/ m1 (- y1 b1)))) +(assert (= b1 1.25)) +(assert (= m1 (/ 1 3))) + +(assert (and (> x x1) (> y y1))) + +(check-sat) +(exit) + diff --git a/test/regress/regress1/arith/arith-int-001.cvc b/test/regress/regress1/arith/arith-int-001.cvc index 03ed1a6ae..3fd528c11 100644 --- a/test/regress/regress1/arith/arith-int-001.cvc +++ b/test/regress/regress1/arith/arith-int-001.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-23 * x0) + (-23 * x1) + (5 * x2) + (-17 * x3) = 7 ; ASSERT (-14 * x0) + (-14 * x1) + (19 * x2) + (-24 * x3) = 29 ; diff --git a/test/regress/regress1/arith/arith-int-002.cvc b/test/regress/regress1/arith/arith-int-002.cvc index 849daba79..6cc4b2c5e 100644 --- a/test/regress/regress1/arith/arith-int-002.cvc +++ b/test/regress/regress1/arith/arith-int-002.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-23 * x1) + (2 * x2) + (-19 * x3) = -18 ; ASSERT (25 * x0) + (23 * x1) + (21 * x2) + (20 * x3) = 2 ; diff --git a/test/regress/regress1/arith/arith-int-003.cvc b/test/regress/regress1/arith/arith-int-003.cvc index 9c060c469..f294babe6 100644 --- a/test/regress/regress1/arith/arith-int-003.cvc +++ b/test/regress/regress1/arith/arith-int-003.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-7 * x1) + (15 * x2) + (21 * x3) = 19 ; ASSERT (6 * x0) + (-24 * x1) + (25 * x2) + (-18 * x3) > -25 ; diff --git a/test/regress/regress1/arith/arith-int-004.cvc b/test/regress/regress1/arith/arith-int-004.cvc index 314b76d18..15b060d92 100644 --- a/test/regress/regress1/arith/arith-int-004.cvc +++ b/test/regress/regress1/arith/arith-int-004.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ; diff --git a/test/regress/regress1/arith/arith-int-005.cvc b/test/regress/regress1/arith/arith-int-005.cvc index 9b9776ad3..3701d60b4 100644 --- a/test/regress/regress1/arith/arith-int-005.cvc +++ b/test/regress/regress1/arith/arith-int-005.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (13 * x0) + (0 * x1) + (6 * x2) + (-30 * x3) = -16 ; ASSERT (-4 * x0) + (-8 * x1) + (14 * x2) + (-8 * x3) = -11 ; diff --git a/test/regress/regress1/arith/arith-int-006.cvc b/test/regress/regress1/arith/arith-int-006.cvc index 999b4a5b4..53a80310a 100644 --- a/test/regress/regress1/arith/arith-int-006.cvc +++ b/test/regress/regress1/arith/arith-int-006.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-7 * x0) + (-28 * x1) + (8 * x2) + (29 * x3) = -18 ; ASSERT (11 * x0) + (2 * x1) + (4 * x2) + (23 * x3) = 6 ; diff --git a/test/regress/regress1/arith/arith-int-007.cvc b/test/regress/regress1/arith/arith-int-007.cvc index 4cb4d88ef..c0732e2b2 100644 --- a/test/regress/regress1/arith/arith-int-007.cvc +++ b/test/regress/regress1/arith/arith-int-007.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (17 * x1) + (30 * x2) + (-31 * x3) <= -20 ; ASSERT (-3 * x0) + (16 * x1) + (20 * x2) + (-25 * x3) < 28 ; diff --git a/test/regress/regress1/arith/arith-int-008.cvc b/test/regress/regress1/arith/arith-int-008.cvc index 1ae22c993..1810d6f28 100644 --- a/test/regress/regress1/arith/arith-int-008.cvc +++ b/test/regress/regress1/arith/arith-int-008.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-12 * x0) + (-15 * x1) + (-31 * x2) + (17 * x3) = -16 ; ASSERT (11 * x0) + (-5 * x1) + (-8 * x2) + (-17 * x3) > -4 ; diff --git a/test/regress/regress1/arith/arith-int-009.cvc b/test/regress/regress1/arith/arith-int-009.cvc index 9bd7a2ce4..14b26da6c 100644 --- a/test/regress/regress1/arith/arith-int-009.cvc +++ b/test/regress/regress1/arith/arith-int-009.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-16 * x0) + (-21 * x1) + (32 * x2) + (32 * x3) = -19 ; ASSERT (-10 * x0) + (-21 * x1) + (13 * x2) + (-7 * x3) = 2 ; diff --git a/test/regress/regress1/arith/arith-int-010.cvc b/test/regress/regress1/arith/arith-int-010.cvc index 4ac85a984..aa649ba4a 100644 --- a/test/regress/regress1/arith/arith-int-010.cvc +++ b/test/regress/regress1/arith/arith-int-010.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-2 * x1) + (-29 * x2) + (-24 * x3) = 3 ; ASSERT (3 * x0) + (11 * x1) + (-14 * x2) + (6 * x3) = 4 ; diff --git a/test/regress/regress1/arith/arith-int-011.cvc b/test/regress/regress1/arith/arith-int-011.cvc index bd2fa2a0d..7de68533f 100644 --- a/test/regress/regress1/arith/arith-int-011.cvc +++ b/test/regress/regress1/arith/arith-int-011.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (13 * x0) + (-1 * x1) + (11 * x2) + (10 * x3) = 9 ; ASSERT (-7 * x0) + (3 * x1) + (-22 * x2) + (16 * x3) >= 9; diff --git a/test/regress/regress1/arith/arith-int-012.cvc b/test/regress/regress1/arith/arith-int-012.cvc index 11b0dab27..10922dd89 100644 --- a/test/regress/regress1/arith/arith-int-012.cvc +++ b/test/regress/regress1/arith/arith-int-012.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (18 * x0) + (32 * x1) + (-11 * x2) + (18 * x3) < -25 ; ASSERT (-31 * x0) + (16 * x1) + (24 * x2) + (9 * x3) >= -24; diff --git a/test/regress/regress1/arith/arith-int-013.cvc b/test/regress/regress1/arith/arith-int-013.cvc index 329251cae..8a1f76add 100644 --- a/test/regress/regress1/arith/arith-int-013.cvc +++ b/test/regress/regress1/arith/arith-int-013.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-14 * x1) + (4 * x2) + (-12 * x3) > 25 ; ASSERT (14 * x0) + (11 * x1) + (32 * x2) + (-8 * x3) >= 2; diff --git a/test/regress/regress1/arith/arith-int-016.cvc b/test/regress/regress1/arith/arith-int-016.cvc index 6774dd2d1..951650461 100644 --- a/test/regress/regress1/arith/arith-int-016.cvc +++ b/test/regress/regress1/arith/arith-int-016.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-4 * x1) + (-20 * x2) + (-26 * x3) = 2 ; ASSERT (13 * x0) + (13 * x1) + (-14 * x2) + (26 * x3) = -8 ; diff --git a/test/regress/regress1/arith/arith-int-017.cvc b/test/regress/regress1/arith/arith-int-017.cvc index e9a06125a..48287249f 100644 --- a/test/regress/regress1/arith/arith-int-017.cvc +++ b/test/regress/regress1/arith/arith-int-017.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (23 * x0) + (-4 * x1) + (-26 * x2) + (-1 * x3) = 10 ; ASSERT (15 * x0) + (31 * x1) + (31 * x2) + (31 * x3) = 13 ; diff --git a/test/regress/regress1/arith/arith-int-018.cvc b/test/regress/regress1/arith/arith-int-018.cvc index 4cb97b77e..cae6fed72 100644 --- a/test/regress/regress1/arith/arith-int-018.cvc +++ b/test/regress/regress1/arith/arith-int-018.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-11 * x0) + (-26 * x1) + (9 * x2) + (32 * x3) = -11 ; ASSERT (-5 * x0) + (-11 * x1) + (-10 * x2) + (-31 * x3) = -23 ; diff --git a/test/regress/regress1/arith/arith-int-019.cvc b/test/regress/regress1/arith/arith-int-019.cvc index cf9ae2d70..a26bbac01 100644 --- a/test/regress/regress1/arith/arith-int-019.cvc +++ b/test/regress/regress1/arith/arith-int-019.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (25 * x0) + (6 * x1) + (-30 * x2) + (29 * x3) = -5 ; ASSERT (14 * x0) + (16 * x1) + (24 * x2) + (-7 * x3) <= 31 ; diff --git a/test/regress/regress1/arith/arith-int-020.cvc b/test/regress/regress1/arith/arith-int-020.cvc index 07a827465..c1416b38f 100644 --- a/test/regress/regress1/arith/arith-int-020.cvc +++ b/test/regress/regress1/arith/arith-int-020.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-32 * x0) + (31 * x1) + (-32 * x2) + (-21 * x3) = 5 ; ASSERT (32 * x0) + (5 * x1) + (23 * x2) + (-16 * x3) = 8 ; diff --git a/test/regress/regress1/arith/arith-int-022.cvc b/test/regress/regress1/arith/arith-int-022.cvc index 584348da4..4612f72c9 100644 --- a/test/regress/regress1/arith/arith-int-022.cvc +++ b/test/regress/regress1/arith/arith-int-022.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18; QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-024.cvc b/test/regress/regress1/arith/arith-int-024.cvc index f57136dd1..73ae7c4ad 100644 --- a/test/regress/regress1/arith/arith-int-024.cvc +++ b/test/regress/regress1/arith/arith-int-024.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5; QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-026.cvc b/test/regress/regress1/arith/arith-int-026.cvc index 9e69aa2d1..52f2478e0 100644 --- a/test/regress/regress1/arith/arith-int-026.cvc +++ b/test/regress/regress1/arith/arith-int-026.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (25 * x1) + (1 * x2) + (-11 * x3) = 19 ; ASSERT (-10 * x0) + (-27 * x1) + (6 * x2) + (6 * x3) = 28 ; diff --git a/test/regress/regress1/arith/arith-int-027.cvc b/test/regress/regress1/arith/arith-int-027.cvc index b45622fea..6c38642d2 100644 --- a/test/regress/regress1/arith/arith-int-027.cvc +++ b/test/regress/regress1/arith/arith-int-027.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (29 * x1) + (-11 * x2) + (24 * x3) = 13 ; ASSERT (16 * x0) + (-20 * x1) + (-5 * x2) + (12 * x3) = 13 ; diff --git a/test/regress/regress1/arith/arith-int-028.cvc b/test/regress/regress1/arith/arith-int-028.cvc index 61fee4203..7e8b78893 100644 --- a/test/regress/regress1/arith/arith-int-028.cvc +++ b/test/regress/regress1/arith/arith-int-028.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-5 * x1) + (-28 * x2) + (16 * x3) = 10 ; ASSERT (3 * x0) + (-20 * x1) + (-11 * x2) + (-2 * x3) = 25 ; diff --git a/test/regress/regress1/arith/arith-int-029.cvc b/test/regress/regress1/arith/arith-int-029.cvc index ee49bbb68..ba49219d8 100644 --- a/test/regress/regress1/arith/arith-int-029.cvc +++ b/test/regress/regress1/arith/arith-int-029.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-29 * x0) + (-17 * x1) + (11 * x2) + (1 * x3) = -15 ; ASSERT (-13 * x0) + (1 * x1) + (-6 * x2) + (-15 * x3) = 32 ; diff --git a/test/regress/regress1/arith/arith-int-030.cvc b/test/regress/regress1/arith/arith-int-030.cvc index 70b6a3785..a6348b107 100644 --- a/test/regress/regress1/arith/arith-int-030.cvc +++ b/test/regress/regress1/arith/arith-int-030.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (26 * x1) + (-11 * x2) + (17 * x3) = 17 ; ASSERT (-15 * x0) + (2 * x1) + (-9 * x2) + (17 * x3) = -11 ; diff --git a/test/regress/regress1/arith/arith-int-031.cvc b/test/regress/regress1/arith/arith-int-031.cvc index 86242f7aa..056ab622e 100644 --- a/test/regress/regress1/arith/arith-int-031.cvc +++ b/test/regress/regress1/arith/arith-int-031.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-24 * x1) + (-31 * x2) + (12 * x3) = -10 ; ASSERT (-4 * x0) + (22 * x1) + (9 * x2) + (17 * x3) > -20 ; diff --git a/test/regress/regress1/arith/arith-int-032.cvc b/test/regress/regress1/arith/arith-int-032.cvc index 1ee4c9844..08c29108e 100644 --- a/test/regress/regress1/arith/arith-int-032.cvc +++ b/test/regress/regress1/arith/arith-int-032.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (4 * x0) + (-29 * x1) + (-9 * x2) + (9 * x3) = 8 ; ASSERT (-26 * x0) + (-26 * x1) + (26 * x2) + (-18 * x3) = -20 ; diff --git a/test/regress/regress1/arith/arith-int-033.cvc b/test/regress/regress1/arith/arith-int-033.cvc index 599ba4e9a..8259a7725 100644 --- a/test/regress/regress1/arith/arith-int-033.cvc +++ b/test/regress/regress1/arith/arith-int-033.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-14 * x0) + (16 * x1) + (-16 * x2) + (0 * x3) = -8 ; ASSERT (3 * x0) + (-20 * x1) + (-12 * x2) + (-3 * x3) = -7 ; diff --git a/test/regress/regress1/arith/arith-int-034.cvc b/test/regress/regress1/arith/arith-int-034.cvc index ec615a785..2b5ae4f4f 100644 --- a/test/regress/regress1/arith/arith-int-034.cvc +++ b/test/regress/regress1/arith/arith-int-034.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-5 * x1) + (30 * x2) + (-24 * x3) = 12 ; ASSERT (24 * x0) + (27 * x1) + (18 * x2) + (-5 * x3) = -16 ; diff --git a/test/regress/regress1/arith/arith-int-035.cvc b/test/regress/regress1/arith/arith-int-035.cvc index e7dee2484..1bad259e2 100644 --- a/test/regress/regress1/arith/arith-int-035.cvc +++ b/test/regress/regress1/arith/arith-int-035.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-3 * x0) + (2 * x1) + (17 * x2) + (-4 * x3) = -17 ; ASSERT (5 * x0) + (-4 * x1) + (22 * x2) + (14 * x3) = -15 ; diff --git a/test/regress/regress1/arith/arith-int-036.cvc b/test/regress/regress1/arith/arith-int-036.cvc index 9594f9586..0eb783815 100644 --- a/test/regress/regress1/arith/arith-int-036.cvc +++ b/test/regress/regress1/arith/arith-int-036.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-9 * x0) + (-21 * x1) + (-25 * x2) + (-1 * x3) = -11 ; ASSERT (31 * x0) + (-18 * x1) + (5 * x2) + (-11 * x3) = 10 ; diff --git a/test/regress/regress1/arith/arith-int-037.cvc b/test/regress/regress1/arith/arith-int-037.cvc index 4d4422d3f..c3ed60011 100644 --- a/test/regress/regress1/arith/arith-int-037.cvc +++ b/test/regress/regress1/arith/arith-int-037.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (12 * x0) + (14 * x1) + (-22 * x2) + (-6 * x3) = 29 ; ASSERT (-9 * x0) + (14 * x1) + (-23 * x2) + (-31 * x3) = 4 ; diff --git a/test/regress/regress1/arith/arith-int-038.cvc b/test/regress/regress1/arith/arith-int-038.cvc index 476133b24..52ac2b1e3 100644 --- a/test/regress/regress1/arith/arith-int-038.cvc +++ b/test/regress/regress1/arith/arith-int-038.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-24 * x0) + (25 * x1) + (28 * x2) + (-31 * x3) = -1 ; ASSERT (29 * x0) + (17 * x1) + (-2 * x2) + (-6 * x3) <= 4 ; diff --git a/test/regress/regress1/arith/arith-int-039.cvc b/test/regress/regress1/arith/arith-int-039.cvc index 9e9235ae8..cecb7f085 100644 --- a/test/regress/regress1/arith/arith-int-039.cvc +++ b/test/regress/regress1/arith/arith-int-039.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (21 * x1) + (-18 * x2) + (21 * x3) = 30 ; ASSERT (-31 * x0) + (22 * x1) + (-20 * x2) + (18 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-040.cvc b/test/regress/regress1/arith/arith-int-040.cvc index 68502349f..f2dff7796 100644 --- a/test/regress/regress1/arith/arith-int-040.cvc +++ b/test/regress/regress1/arith/arith-int-040.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-1 * x0) + (-24 * x1) + (3 * x2) + (-8 * x3) > -5 ; ASSERT (29 * x0) + (17 * x1) + (-26 * x2) + (20 * x3) > 11 ; diff --git a/test/regress/regress1/arith/arith-int-041.cvc b/test/regress/regress1/arith/arith-int-041.cvc index a0c2dc0f9..9df03a9bd 100644 --- a/test/regress/regress1/arith/arith-int-041.cvc +++ b/test/regress/regress1/arith/arith-int-041.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (8 * x1) + (16 * x2) + (5 * x3) >= 1 ; ASSERT (-30 * x0) + (13 * x1) + (-17 * x2) + (13 * x3) < -24 ; diff --git a/test/regress/regress1/arith/arith-int-043.cvc b/test/regress/regress1/arith/arith-int-043.cvc index 7efea85e5..7a2d6d6af 100644 --- a/test/regress/regress1/arith/arith-int-043.cvc +++ b/test/regress/regress1/arith/arith-int-043.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-23 * x1) + (29 * x2) + (-4 * x3) = 25 ; ASSERT (20 * x0) + (-19 * x1) + (3 * x2) + (-1 * x3) <= -8 ; diff --git a/test/regress/regress1/arith/arith-int-044.cvc b/test/regress/regress1/arith/arith-int-044.cvc index f933b014b..649532a4b 100644 --- a/test/regress/regress1/arith/arith-int-044.cvc +++ b/test/regress/regress1/arith/arith-int-044.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed %%%% down from 24, up from 6, up from 39 x0, x1, x2, x3 : INT; ASSERT (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0; diff --git a/test/regress/regress1/arith/arith-int-045.cvc b/test/regress/regress1/arith/arith-int-045.cvc index ca1a12ba6..2c552c915 100644 --- a/test/regress/regress1/arith/arith-int-045.cvc +++ b/test/regress/regress1/arith/arith-int-045.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-5 * x1) + (-5 * x2) + (25 * x3) = 22 ; ASSERT (2 * x0) + (-25 * x1) + (4 * x2) + (-21 * x3) >= 0 ; diff --git a/test/regress/regress1/arith/arith-int-046.cvc b/test/regress/regress1/arith/arith-int-046.cvc index d4d206c6e..acf4dc9a9 100644 --- a/test/regress/regress1/arith/arith-int-046.cvc +++ b/test/regress/regress1/arith/arith-int-046.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ; ASSERT (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ; diff --git a/test/regress/regress1/arith/arith-int-047.cvc b/test/regress/regress1/arith/arith-int-047.cvc index 0763e5dc3..bb1225b9d 100644 --- a/test/regress/regress1/arith/arith-int-047.cvc +++ b/test/regress/regress1/arith/arith-int-047.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-14 * x0) + (27 * x1) + (10 * x2) + (1 * x3) = 10; ASSERT (-29 * x0) + (-26 * x1) + (-16 * x2) + (17 * x3) >= 16 ; diff --git a/test/regress/regress1/arith/arith-int-048.cvc b/test/regress/regress1/arith/arith-int-048.cvc index e7c05332d..ccc84f389 100644 --- a/test/regress/regress1/arith/arith-int-048.cvc +++ b/test/regress/regress1/arith/arith-int-048.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-11 * x1) + (-14 * x2) + (21 * x3) = 6 ; ASSERT (7 * x0) + (5 * x1) + (13 * x2) + (21 * x3) <= 27 ; diff --git a/test/regress/regress1/arith/arith-int-049.cvc b/test/regress/regress1/arith/arith-int-049.cvc index 8eabc78a8..72e3b7f31 100644 --- a/test/regress/regress1/arith/arith-int-049.cvc +++ b/test/regress/regress1/arith/arith-int-049.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-15 * x0) + (-20 * x1) + (-32 * x2) + (-16 * x3) = -19 ; ASSERT (24 * x0) + (23 * x1) + (22 * x2) + (30 * x3) >= 19 ; diff --git a/test/regress/regress1/arith/arith-int-050.cvc b/test/regress/regress1/arith/arith-int-050.cvc index f0ba939b7..21dbfe09a 100644 --- a/test/regress/regress1/arith/arith-int-050.cvc +++ b/test/regress/regress1/arith/arith-int-050.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-19 * x1) + (6 * x2) + (32 * x3) > 16 ; ASSERT (-1 * x0) + (-30 * x1) + (15 * x2) + (7 * x3) < -10 ; diff --git a/test/regress/regress1/arith/arith-int-051.cvc b/test/regress/regress1/arith/arith-int-051.cvc index 9a2497432..68654a7df 100644 --- a/test/regress/regress1/arith/arith-int-051.cvc +++ b/test/regress/regress1/arith/arith-int-051.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (7 * x1) + (-3 * x2) + (9 * x3) = -3 ; ASSERT (17 * x0) + (-22 * x1) + (-15 * x2) + (-21 * x3) >= 9 ; diff --git a/test/regress/regress1/arith/arith-int-052.cvc b/test/regress/regress1/arith/arith-int-052.cvc index 83fdc89c8..9c9433ede 100644 --- a/test/regress/regress1/arith/arith-int-052.cvc +++ b/test/regress/regress1/arith/arith-int-052.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (-23 * x1) + (11 * x2) + (10 * x3) = 7 ; ASSERT (32 * x0) + (-15 * x1) + (-1 * x2) + (29 * x3) > -25 ; diff --git a/test/regress/regress1/arith/arith-int-053.cvc b/test/regress/regress1/arith/arith-int-053.cvc index fa38fa3da..544d53fb9 100644 --- a/test/regress/regress1/arith/arith-int-053.cvc +++ b/test/regress/regress1/arith/arith-int-053.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (21 * x1) + (23 * x2) + (-20 * x3) = -8 ; ASSERT (-31 * x0) + (-15 * x1) + (-23 * x2) + (29 * x3) = 17; diff --git a/test/regress/regress1/arith/arith-int-054.cvc b/test/regress/regress1/arith/arith-int-054.cvc index 9b0066966..5b4181a11 100644 --- a/test/regress/regress1/arith/arith-int-054.cvc +++ b/test/regress/regress1/arith/arith-int-054.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-29 * x1) + (6 * x2) + (8 * x3) = -10 ; ASSERT (0 * x0) + (8 * x1) + (-20 * x2) + (12 * x3) = 16 ; diff --git a/test/regress/regress1/arith/arith-int-055.cvc b/test/regress/regress1/arith/arith-int-055.cvc index 9729fb565..fdfa45848 100644 --- a/test/regress/regress1/arith/arith-int-055.cvc +++ b/test/regress/regress1/arith/arith-int-055.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-21 * x0) + (-4 * x1) + (-28 * x2) + (-7 * x3) = -23 ; ASSERT (-7 * x0) + (-21 * x1) + (29 * x2) + (11 * x3) = 29 ; diff --git a/test/regress/regress1/arith/arith-int-056.cvc b/test/regress/regress1/arith/arith-int-056.cvc index e1c3ee1da..394b3dd4e 100644 --- a/test/regress/regress1/arith/arith-int-056.cvc +++ b/test/regress/regress1/arith/arith-int-056.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (23 * x1) + (29 * x2) + (21 * x3) = -2 ; ASSERT (1 * x0) + (10 * x1) + (-32 * x2) + (-17 * x3) = -2 ; diff --git a/test/regress/regress1/arith/arith-int-057.cvc b/test/regress/regress1/arith/arith-int-057.cvc index 4e7b939b4..252601514 100644 --- a/test/regress/regress1/arith/arith-int-057.cvc +++ b/test/regress/regress1/arith/arith-int-057.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (10 * x1) + (-25 * x2) + (-10 * x3) = -18 ; ASSERT (27 * x0) + (5 * x1) + (8 * x2) + (13 * x3) = -8; diff --git a/test/regress/regress1/arith/arith-int-058.cvc b/test/regress/regress1/arith/arith-int-058.cvc index 4d964f1c6..7e2a04d45 100644 --- a/test/regress/regress1/arith/arith-int-058.cvc +++ b/test/regress/regress1/arith/arith-int-058.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-15 * x0) + (3 * x1) + (31 * x2) + (2 * x3) = -18 ; ASSERT (-25 * x0) + (-10 * x1) + (15 * x2) + (29 * x3) = -18 ; diff --git a/test/regress/regress1/arith/arith-int-059.cvc b/test/regress/regress1/arith/arith-int-059.cvc index 841d9c8e1..87773679e 100644 --- a/test/regress/regress1/arith/arith-int-059.cvc +++ b/test/regress/regress1/arith/arith-int-059.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (31 * x0) + (-19 * x1) + (0 * x2) + (32 * x3) = -14 ; ASSERT (12 * x0) + (-25 * x1) + (-32 * x2) + (-18 * x3) = 18 ; diff --git a/test/regress/regress1/arith/arith-int-060.cvc b/test/regress/regress1/arith/arith-int-060.cvc index 227cb49b1..74dd16dca 100644 --- a/test/regress/regress1/arith/arith-int-060.cvc +++ b/test/regress/regress1/arith/arith-int-060.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (3 * x0) + (8 * x1) + (26 * x2) + (-17 * x3) = 31 ; ASSERT (-14 * x0) + (25 * x1) + (4 * x2) + (-8 * x3) = 15 ; diff --git a/test/regress/regress1/arith/arith-int-061.cvc b/test/regress/regress1/arith/arith-int-061.cvc index 4a3cc28d0..b3bd247b2 100644 --- a/test/regress/regress1/arith/arith-int-061.cvc +++ b/test/regress/regress1/arith/arith-int-061.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (16 * x0) + (20 * x1) + (-8 * x2) + (-27 * x3) = -2 ; ASSERT (15 * x0) + (9 * x1) + (-1 * x2) + (4 * x3) = 1 ; diff --git a/test/regress/regress1/arith/arith-int-062.cvc b/test/regress/regress1/arith/arith-int-062.cvc index f9a3156a2..0a185eb68 100644 --- a/test/regress/regress1/arith/arith-int-062.cvc +++ b/test/regress/regress1/arith/arith-int-062.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (11 * x0) + (22 * x1) + (19 * x2) + (-8 * x3) = 12 ; ASSERT (23 * x0) + (-6 * x1) + (-5 * x2) + (26 * x3) = 0 ; diff --git a/test/regress/regress1/arith/arith-int-063.cvc b/test/regress/regress1/arith/arith-int-063.cvc index d88104688..13c4aae2e 100644 --- a/test/regress/regress1/arith/arith-int-063.cvc +++ b/test/regress/regress1/arith/arith-int-063.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (20 * x0) + (-10 * x1) + (-10 * x2) + (26 * x3) = -9 ; ASSERT (10 * x0) + (0 * x1) + (16 * x2) + (7 * x3) = 7 ; diff --git a/test/regress/regress1/arith/arith-int-064.cvc b/test/regress/regress1/arith/arith-int-064.cvc index 21ca822e1..f50b3cd97 100644 --- a/test/regress/regress1/arith/arith-int-064.cvc +++ b/test/regress/regress1/arith/arith-int-064.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (-11 * x1) + (27 * x2) + (4 * x3) = 6 ; ASSERT (32 * x0) + (27 * x1) + (31 * x2) + (-13 * x3) = 21 ; diff --git a/test/regress/regress1/arith/arith-int-065.cvc b/test/regress/regress1/arith/arith-int-065.cvc index b1b9e1b51..354eb981c 100644 --- a/test/regress/regress1/arith/arith-int-065.cvc +++ b/test/regress/regress1/arith/arith-int-065.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (3 * x0) + (-21 * x1) + (-3 * x2) + (6 * x3) = -18 ; ASSERT (-15 * x0) + (19 * x1) + (-21 * x2) + (-29 * x3) = -8 ; diff --git a/test/regress/regress1/arith/arith-int-066.cvc b/test/regress/regress1/arith/arith-int-066.cvc index 9532b4198..f53a254bd 100644 --- a/test/regress/regress1/arith/arith-int-066.cvc +++ b/test/regress/regress1/arith/arith-int-066.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (28 * x0) + (-8 * x1) + (32 * x2) + (-3 * x3) = -18 ; ASSERT (-4 * x0) + (5 * x1) + (-2 * x2) + (-17 * x3) > 19 ; diff --git a/test/regress/regress1/arith/arith-int-067.cvc b/test/regress/regress1/arith/arith-int-067.cvc index 5d7b52e69..61159e9aa 100644 --- a/test/regress/regress1/arith/arith-int-067.cvc +++ b/test/regress/regress1/arith/arith-int-067.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-25 * x0) + (-32 * x1) + (-29 * x2) + (-9 * x3) = -2 ; ASSERT (22 * x0) + (10 * x1) + (-18 * x2) + (2 * x3) = -17 ; diff --git a/test/regress/regress1/arith/arith-int-068.cvc b/test/regress/regress1/arith/arith-int-068.cvc index 107a21a12..683d36801 100644 --- a/test/regress/regress1/arith/arith-int-068.cvc +++ b/test/regress/regress1/arith/arith-int-068.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (-8 * x1) + (5 * x2) + (-7 * x3) = -7 ; ASSERT (-30 * x0) + (24 * x1) + (-4 * x2) + (-30 * x3) = 22 ; diff --git a/test/regress/regress1/arith/arith-int-069.cvc b/test/regress/regress1/arith/arith-int-069.cvc index 3fab229b0..356a28013 100644 --- a/test/regress/regress1/arith/arith-int-069.cvc +++ b/test/regress/regress1/arith/arith-int-069.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-12 * x0) + (20 * x1) + (2 * x2) + (-24 * x3) = 16 ; ASSERT (-32 * x0) + (27 * x1) + (1 * x2) + (-3 * x3) = -3 ; diff --git a/test/regress/regress1/arith/arith-int-070.cvc b/test/regress/regress1/arith/arith-int-070.cvc index cd828da5f..791b3b8af 100644 --- a/test/regress/regress1/arith/arith-int-070.cvc +++ b/test/regress/regress1/arith/arith-int-070.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (0 * x0) + (-16 * x1) + (14 * x2) + (20 * x3) = 1 ; ASSERT (-27 * x0) + (-5 * x1) + (-22 * x2) + (-24 * x3) = -7 ; diff --git a/test/regress/regress1/arith/arith-int-071.cvc b/test/regress/regress1/arith/arith-int-071.cvc index ce5336476..d44b18b45 100644 --- a/test/regress/regress1/arith/arith-int-071.cvc +++ b/test/regress/regress1/arith/arith-int-071.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (3 * x1) + (-17 * x2) + (-21 * x3) = -9 ; ASSERT (-12 * x0) + (-9 * x1) + (-9 * x2) + (-16 * x3) = -12 ; diff --git a/test/regress/regress1/arith/arith-int-072.cvc b/test/regress/regress1/arith/arith-int-072.cvc index 10222deae..fb13a6616 100644 --- a/test/regress/regress1/arith/arith-int-072.cvc +++ b/test/regress/regress1/arith/arith-int-072.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (1 * x0) + (-1 * x1) + (-16 * x2) + (6 * x3) = -11 ; ASSERT (-17 * x0) + (17 * x1) + (-15 * x2) + (24 * x3) = -21 ; diff --git a/test/regress/regress1/arith/arith-int-073.cvc b/test/regress/regress1/arith/arith-int-073.cvc index 98e74be8f..784190cad 100644 --- a/test/regress/regress1/arith/arith-int-073.cvc +++ b/test/regress/regress1/arith/arith-int-073.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (8 * x0) + (-14 * x1) + (0 * x2) + (7 * x3) = 26 ; ASSERT (-7 * x0) + (-14 * x1) + (15 * x2) + (31 * x3) = 8 ; diff --git a/test/regress/regress1/arith/arith-int-074.cvc b/test/regress/regress1/arith/arith-int-074.cvc index 28cc48186..914cbe8e3 100644 --- a/test/regress/regress1/arith/arith-int-074.cvc +++ b/test/regress/regress1/arith/arith-int-074.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (14 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) = -18 ; ASSERT (-11 * x0) + (12 * x1) + (8 * x2) + (-1 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-075.cvc b/test/regress/regress1/arith/arith-int-075.cvc index 3b5131e8b..d3851e284 100644 --- a/test/regress/regress1/arith/arith-int-075.cvc +++ b/test/regress/regress1/arith/arith-int-075.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (29 * x1) + (15 * x2) + (32 * x3) = 32 ; ASSERT (18 * x0) + (-8 * x1) + (18 * x2) + (22 * x3) = 20 ; diff --git a/test/regress/regress1/arith/arith-int-076.cvc b/test/regress/regress1/arith/arith-int-076.cvc index 2c8de7cdf..25a3a7d35 100644 --- a/test/regress/regress1/arith/arith-int-076.cvc +++ b/test/regress/regress1/arith/arith-int-076.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (29 * x3) = -15 ; ASSERT (3 * x0) + (19 * x1) + (21 * x2) + (-32 * x3) = 11 ; diff --git a/test/regress/regress1/arith/arith-int-077.cvc b/test/regress/regress1/arith/arith-int-077.cvc index d14da386e..7e4482093 100644 --- a/test/regress/regress1/arith/arith-int-077.cvc +++ b/test/regress/regress1/arith/arith-int-077.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (26 * x0) + (-28 * x1) + (27 * x2) + (8 * x3) = 31 ; ASSERT (-32 * x0) + (11 * x1) + (-5 * x2) + (14 * x3) = 2; diff --git a/test/regress/regress1/arith/arith-int-078.cvc b/test/regress/regress1/arith/arith-int-078.cvc index 3197c6524..eacccc375 100644 --- a/test/regress/regress1/arith/arith-int-078.cvc +++ b/test/regress/regress1/arith/arith-int-078.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (17 * x0) + (-14 * x1) + (13 * x2) + (13 * x3) = -18 ; ASSERT (13 * x0) + (16 * x1) + (-12 * x2) + (19 * x3) = -20 ; diff --git a/test/regress/regress1/arith/arith-int-080.cvc b/test/regress/regress1/arith/arith-int-080.cvc index 8be0f9a73..bf6b90c67 100644 --- a/test/regress/regress1/arith/arith-int-080.cvc +++ b/test/regress/regress1/arith/arith-int-080.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (5 * x0) + (-17 * x1) + (15 * x2) + (-15 * x3) = -14 ; ASSERT (-28 * x0) + (-17 * x1) + (-29 * x2) + (-19 * x3) = 14; diff --git a/test/regress/regress1/arith/arith-int-081.cvc b/test/regress/regress1/arith/arith-int-081.cvc index 546148376..47cc66ae2 100644 --- a/test/regress/regress1/arith/arith-int-081.cvc +++ b/test/regress/regress1/arith/arith-int-081.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-8 * x0) + (31 * x1) + (-23 * x2) + (-8 * x3) = 8; ASSERT (24 * x0) + (-2 * x1) + (2 * x2) + (-2 * x3) >= -17 ; diff --git a/test/regress/regress1/arith/arith-int-082.cvc b/test/regress/regress1/arith/arith-int-082.cvc index 62bd45de7..a6245f036 100644 --- a/test/regress/regress1/arith/arith-int-082.cvc +++ b/test/regress/regress1/arith/arith-int-082.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-29 * x0) + (-3 * x1) + (27 * x2) + (13 * x3) = -10 ; ASSERT (7 * x0) + (-17 * x1) + (11 * x2) + (-30 * x3) <= 6 ; diff --git a/test/regress/regress1/arith/arith-int-083.cvc b/test/regress/regress1/arith/arith-int-083.cvc index 6b1084353..3a7c635cc 100644 --- a/test/regress/regress1/arith/arith-int-083.cvc +++ b/test/regress/regress1/arith/arith-int-083.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-31 * x1) + (31 * x2) + (28 * x3) = -13 ; ASSERT (1 * x0) + (13 * x1) + (12 * x2) + (-15 * x3) > -8 ; diff --git a/test/regress/regress1/arith/arith-int-084.cvc b/test/regress/regress1/arith/arith-int-084.cvc index 5f0e17afe..d4a0a966c 100644 --- a/test/regress/regress1/arith/arith-int-084.cvc +++ b/test/regress/regress1/arith/arith-int-084.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-2 * x0) + (-13 * x1) + (-14 * x2) + (-26 * x3) <= 4 ; ASSERT (-17 * x0) + (-17 * x1) + (21 * x2) + (-4 * x3) < 18 ; diff --git a/test/regress/regress1/arith/arith-int-085.cvc b/test/regress/regress1/arith/arith-int-085.cvc index 74dd714e8..b1a343e73 100644 --- a/test/regress/regress1/arith/arith-int-085.cvc +++ b/test/regress/regress1/arith/arith-int-085.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed %% down from 3 x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ; diff --git a/test/regress/regress1/arith/arith-int-086.cvc b/test/regress/regress1/arith/arith-int-086.cvc index 64c212b3c..6ee96589b 100644 --- a/test/regress/regress1/arith/arith-int-086.cvc +++ b/test/regress/regress1/arith/arith-int-086.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-16 * x0) + (28 * x1) + (2 * x2) + (7 * x3) = -25 ; ASSERT (-20 * x0) + (-24 * x1) + (4 * x2) + (32 * x3) = -22 ; diff --git a/test/regress/regress1/arith/arith-int-087.cvc b/test/regress/regress1/arith/arith-int-087.cvc index 312c08917..b969df1a3 100644 --- a/test/regress/regress1/arith/arith-int-087.cvc +++ b/test/regress/regress1/arith/arith-int-087.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-4 * x0) + (25 * x1) + (-2 * x2) + (-16 * x3) = 27 ; ASSERT (-11 * x0) + (26 * x1) + (18 * x2) + (-18 * x3) = -15 ; diff --git a/test/regress/regress1/arith/arith-int-088.cvc b/test/regress/regress1/arith/arith-int-088.cvc index 5212640be..de0d23844 100644 --- a/test/regress/regress1/arith/arith-int-088.cvc +++ b/test/regress/regress1/arith/arith-int-088.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (-9 * x1) + (-27 * x2) + (9 * x3) = -1 ; ASSERT (-26 * x0) + (11 * x1) + (23 * x2) + (-5 * x3) >= 20 ; diff --git a/test/regress/regress1/arith/arith-int-089.cvc b/test/regress/regress1/arith/arith-int-089.cvc index 7ff36d29e..e50daa9de 100644 --- a/test/regress/regress1/arith/arith-int-089.cvc +++ b/test/regress/regress1/arith/arith-int-089.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (14 * x0) + (-14 * x1) + (-29 * x2) + (31 * x3) = -15 ; ASSERT (-14 * x0) + (2 * x1) + (26 * x2) + (29 * x3) = 25 ; diff --git a/test/regress/regress1/arith/arith-int-090.cvc b/test/regress/regress1/arith/arith-int-090.cvc index 52b9c13f0..74d4ba4db 100644 --- a/test/regress/regress1/arith/arith-int-090.cvc +++ b/test/regress/regress1/arith/arith-int-090.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-13 * x0) + (-14 * x1) + (-10 * x2) + (32 * x3) = 11 ; ASSERT (28 * x0) + (21 * x1) + (-20 * x2) + (-32 * x3) > -31 ; diff --git a/test/regress/regress1/arith/arith-int-091.cvc b/test/regress/regress1/arith/arith-int-091.cvc index 29a19db39..c03b544a3 100644 --- a/test/regress/regress1/arith/arith-int-091.cvc +++ b/test/regress/regress1/arith/arith-int-091.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (26 * x0) + (32 * x1) + (-26 * x2) + (-26 * x3) = -26 ; ASSERT (30 * x0) + (17 * x1) + (28 * x2) + (-9 * x3) = -21 ; diff --git a/test/regress/regress1/arith/arith-int-092.cvc b/test/regress/regress1/arith/arith-int-092.cvc index 51c8a6bc4..d080cde0c 100644 --- a/test/regress/regress1/arith/arith-int-092.cvc +++ b/test/regress/regress1/arith/arith-int-092.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-20 * x0) + (19 * x1) + (16 * x2) + (-27 * x3) = -22 ; ASSERT (12 * x0) + (-18 * x1) + (-25 * x2) + (-1 * x3) = -22 ; diff --git a/test/regress/regress1/arith/arith-int-093.cvc b/test/regress/regress1/arith/arith-int-093.cvc index 7d2123d41..e910def47 100644 --- a/test/regress/regress1/arith/arith-int-093.cvc +++ b/test/regress/regress1/arith/arith-int-093.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (22 * x0) + (-2 * x1) + (-1 * x2) + (-24 * x3) = 8 ; ASSERT (-6 * x0) + (9 * x1) + (-20 * x2) + (-23 * x3) = 14 ; diff --git a/test/regress/regress1/arith/arith-int-094.cvc b/test/regress/regress1/arith/arith-int-094.cvc index a5f1aefce..2204bba4e 100644 --- a/test/regress/regress1/arith/arith-int-094.cvc +++ b/test/regress/regress1/arith/arith-int-094.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-7 * x0) + (-11 * x1) + (26 * x2) + (10 * x3) = 31 ; ASSERT (-17 * x0) + (-20 * x1) + (24 * x2) + (-9 * x3) = -32 ; diff --git a/test/regress/regress1/arith/arith-int-095.cvc b/test/regress/regress1/arith/arith-int-095.cvc index bc47d6f49..e803dbe9b 100644 --- a/test/regress/regress1/arith/arith-int-095.cvc +++ b/test/regress/regress1/arith/arith-int-095.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (2 * x0) + (28 * x1) + (3 * x2) + (8 * x3) > -32 ; ASSERT (-15 * x0) + (21 * x1) + (-11 * x2) + (28 * x3) <= -19 ; diff --git a/test/regress/regress1/arith/arith-int-096.cvc b/test/regress/regress1/arith/arith-int-096.cvc index 2f6cf3155..354ae180d 100644 --- a/test/regress/regress1/arith/arith-int-096.cvc +++ b/test/regress/regress1/arith/arith-int-096.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (23 * x0) + (24 * x1) + (19 * x2) + (-3 * x3) = -16 ; ASSERT (2 * x0) + (-13 * x1) + (5 * x2) + (-1 * x3) = 28; diff --git a/test/regress/regress1/arith/arith-int-097.cvc b/test/regress/regress1/arith/arith-int-097.cvc index b05061192..67eb614eb 100644 --- a/test/regress/regress1/arith/arith-int-097.cvc +++ b/test/regress/regress1/arith/arith-int-097.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (19 * x0) + (-11 * x1) + (-19 * x2) + (5 * x3) = 26 ; ASSERT (1 * x0) + (-28 * x1) + (-2 * x2) + (15 * x3) < 9 ; diff --git a/test/regress/regress1/arith/arith-int-099.cvc b/test/regress/regress1/arith/arith-int-099.cvc index 0d74dcb39..57a45de03 100644 --- a/test/regress/regress1/arith/arith-int-099.cvc +++ b/test/regress/regress1/arith/arith-int-099.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-31 * x0) + (-20 * x1) + (-30 * x2) + (-28 * x3) = -24 ; ASSERT (11 * x0) + (-32 * x1) + (-2 * x2) + (8 * x3) <= 16 ; diff --git a/test/regress/regress1/arith/arith-int-100.cvc b/test/regress/regress1/arith/arith-int-100.cvc index 7e07bee14..66be1f8f7 100644 --- a/test/regress/regress1/arith/arith-int-100.cvc +++ b/test/regress/regress1/arith/arith-int-100.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ; ASSERT (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ; diff --git a/test/regress/regress1/arith/bug547.1.smt2 b/test/regress/regress1/arith/bug547.1.smt2 index 4b7cf9780..38d1dfcb1 100644 --- a/test/regress/regress1/arith/bug547.1.smt2 +++ b/test/regress/regress1/arith/bug547.1.smt2 @@ -1,5 +1,5 @@ -; COMMAND-LINE: --rewrite-divk -; EXPECT: unknown +; COMMAND-LINE: --rewrite-divk --nl-ext-tplanes +; EXPECT: sat (set-logic QF_NIA) (declare-fun x () Int) (declare-fun y () Int) diff --git a/test/regress/regress1/boolean.cvc b/test/regress/regress1/boolean.cvc index eb0e7ab52..2c861c0f0 100644 --- a/test/regress/regress1/boolean.cvc +++ b/test/regress/regress1/boolean.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed p : BOOLEAN; q : BOOLEAN; r : BOOLEAN; diff --git a/test/regress/regress1/fmf/fmf-strange-bounds.smt2 b/test/regress/regress1/fmf/fmf-strange-bounds.smt2 index 7812c2431..20738245c 100644 --- a/test/regress/regress1/fmf/fmf-strange-bounds.smt2 +++ b/test/regress/regress1/fmf/fmf-strange-bounds.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --fmf-bound +; COMMAND-LINE: --fmf-bound --finite-model-find ; EXPECT: sat (set-logic ALL) (set-info :status sat) @@ -17,11 +17,16 @@ (assert (>= (h (g 77)) 2)) (assert (not (= (g 77) (f 77)))) -(assert (forall ((x Int) (y Int) (z U)) (=> +(assert (forall ((x Int) (z U)) (=> (or (= z (f x)) (= z (g x))) (=> (member x S) -(=> (and (<= 0 y) (<= y (h z))) -(P x y z)))))) +(P x 0 z))))) + +(assert (forall ((x Int) (y Int) (z U)) (=> +(or (= x 5) (= x 6)) +(=> (and (<= 0 y) (<= y x)) +(P x y z))))) + (declare-fun Q (U Int) Bool) diff --git a/test/regress/regress1/fmf/ko-bound-set.cvc b/test/regress/regress1/fmf/ko-bound-set.cvc index eebcbc2f8..5306a1513 100644 --- a/test/regress/regress1/fmf/ko-bound-set.cvc +++ b/test/regress/regress1/fmf/ko-bound-set.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed OPTION "finite-model-find"; OPTION "fmf-bound-int"; OPTION "produce-models"; diff --git a/test/regress/regress1/hole6.cvc b/test/regress/regress1/hole6.cvc index dfa9b72d5..5ec31d801 100644 --- a/test/regress/regress1/hole6.cvc +++ b/test/regress/regress1/hole6.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x_1 : BOOLEAN; x_2 : BOOLEAN; x_3 : BOOLEAN; diff --git a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc index f7407a2a5..6f2a8764b 100644 --- a/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc +++ b/test/regress/regress1/quantifiers/set-choice-koikonomou.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed OPTION "finite-model-find"; OPTION "fmf-bound-int"; diff --git a/test/regress/regress1/rr-verify/regex.sy b/test/regress/regress1/rr-verify/regex.sy index 6c6da3dd2..2d911e56a 100644 --- a/test/regress/regress1/rr-verify/regex.sy +++ b/test/regress/regress1/rr-verify/regex.sy @@ -1,17 +1,18 @@ -; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break +; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.") ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)' ; EXIT: 1 (set-logic SLIA) -(synth-fun f ((x String) (y String)) Bool ( +(synth-fun f ((x String) (y String)) Bool +((Start Bool) (StartRe RegLan) (StartStr String)) ( (Start Bool ( true false (= StartStr StartStr) - (str.in.re StartStr StartRe) + (str.in_re StartStr StartRe) )) (StartRe RegLan ( @@ -19,7 +20,7 @@ (re.++ StartRe StartRe) (re.union StartRe StartRe) (re.* StartRe) - (str.to.re StartStr) + (str.to_re StartStr) )) (StartStr String ( diff --git a/test/regress/regress1/strings/bug686dd.smt2 b/test/regress/regress1/strings/bug686dd.smt2 index 0cb9fac26..b5c9457ff 100644 --- a/test/regress/regress1/strings/bug686dd.smt2 +++ b/test/regress/regress1/strings/bug686dd.smt2 @@ -8,7 +8,7 @@ (declare-fun root6 () T) (assert (and -(str.in.re root5 (re.loop (re.range "0" "9") 4 4) ) -(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) ) +(str.in.re root5 ((_ re.loop 4 4) (re.range "0" "9")) ) +(str.in.re (TCb root6) ((_ re.loop 4 4) (re.range "0" "9")) ) ) ) (check-sat) diff --git a/test/regress/regress1/strings/pierre150331.smt2 b/test/regress/regress1/strings/pierre150331.smt2 index add60d534..e04db8e9a 100644 --- a/test/regress/regress1/strings/pierre150331.smt2 +++ b/test/regress/regress1/strings/pierre150331.smt2 @@ -6,7 +6,7 @@ (define-fun stringEval ((?s String)) Bool (str.in.re ?s
(re.union
(str.to.re "H")
-(re.++ (re.loop (str.to.re "{") 2 2 ) (re.loop (re.union re.nostr (re.range " " "]") (re.range "" "^") ) 2 4 ) ) ) ) )
+(re.++ ((_ re.loop 2 2) (str.to.re "{") ) ((_ re.loop 2 4) (re.union re.nostr (re.range " " "]") (re.range "" "^") ) ) ) ) ) )
(declare-fun s0() String)
(declare-fun s1() String)
(declare-fun s2() String)
diff --git a/test/regress/regress1/strings/reloop.smt2 b/test/regress/regress1/strings/reloop.smt2 index 22537b957..6230d1656 100644 --- a/test/regress/regress1/strings/reloop.smt2 +++ b/test/regress/regress1/strings/reloop.smt2 @@ -8,11 +8,11 @@ (declare-fun z () String) (declare-fun w () String) -(assert (str.in.re x (re.loop (str.to.re "a") 5))) -(assert (str.in.re y (re.loop (str.to.re "b") 2 5))) -(assert (str.in.re z (re.loop (str.to.re "c") 5))) +(assert (str.in.re x ((_ re.^ 5) (str.to.re "a")))) +(assert (str.in.re y ((_ re.loop 2 5) (str.to.re "b")))) +(assert (str.in.re z ((_ re.loop 5 15) (str.to.re "c")))) (assert (> (str.len z) 7)) -(assert (str.in.re w (re.loop (str.to.re "b") 2 7))) +(assert (str.in.re w ((_ re.loop 2 7) (str.to.re "b")))) (assert (> (str.len w) 2)) (assert (< (str.len w) 5)) diff --git a/test/regress/regress1/sygus/dt-test-ns.sy b/test/regress/regress1/sygus/dt-test-ns.sy index 3d078cc25..90fa57827 100644 --- a/test/regress/regress1/sygus/dt-test-ns.sy +++ b/test/regress/regress1/sygus/dt-test-ns.sy @@ -1,6 +1,6 @@ ; EXPECT: unsat ; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status -(set-logic LIA) +(set-logic DTLIA) (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil)))) @@ -8,6 +8,6 @@ (declare-var x Int) -(constraint (is-cons (f x))) +(constraint ((_ is cons) (f x))) (constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x))))))) (check-synth) diff --git a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy index abcfc2217..089a8f11f 100644 --- a/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy +++ b/test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy @@ -1,14 +1,15 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic BV) -(define-fun hd19 ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) - (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m)))) +(define-fun hd19 ((x (_ BitVec 32)) (m (_ BitVec 32)) (k (_ BitVec 32))) (_ BitVec 32) + (bvxor x (bvxor (bvshl (bvand (bvxor (bvlshr x k) x) m) k) (bvand (bvxor (bvlshr x k) x) m)))) ; bvand is a duplicate -(synth-fun f ((x (BitVec 32)) (m (BitVec 32)) (k (BitVec 32))) (BitVec 32) - ((Start (BitVec 32) ((bvand Start Start) +(synth-fun f ((x (_ BitVec 32)) (m (_ BitVec 32)) (k (_ BitVec 32))) (_ BitVec 32) + ((Start (_ BitVec 32))) + ((Start (_ BitVec 32) ((bvand Start Start) (bvsub Start Start) (bvxor Start Start) (bvor Start Start) @@ -23,10 +24,9 @@ k)))) -(declare-var x (BitVec 32)) -(declare-var m (BitVec 32)) -(declare-var k (BitVec 32)) +(declare-var x (_ BitVec 32)) +(declare-var m (_ BitVec 32)) +(declare-var k (_ BitVec 32)) (constraint (= (hd19 x m k) (f x m k))) (check-synth) - diff --git a/test/regress/regress1/sygus/issue3461.sy b/test/regress/regress1/sygus/issue3461.sy index 1f839c229..08b5738c1 100644 --- a/test/regress/regress1/sygus/issue3461.sy +++ b/test/regress/regress1/sygus/issue3461.sy @@ -1,15 +1,16 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic ALL_SUPPORTED) (declare-datatype Doc ((D (owner Int) (body Int)))) -(declare-datatype Policy - ((p (principal Int)) +(declare-datatype Policy + ((p (principal Int)) (por (left Policy) (right Policy)))) (synth-fun mkPolicy ((d Doc)) Policy + ((Start Policy) (Q Policy)) ((Start Policy (Q)) (Q Policy ((p 0) (p 1) (por Q Q)))) ) diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy index 83ac8290d..ae2bcc00e 100644 --- a/test/regress/regress1/sygus/list-head-x.sy +++ b/test/regress/regress1/sygus/list-head-x.sy @@ -8,6 +8,6 @@ (declare-var x Int) -(constraint (is-cons (f x))) +(constraint ((_ is cons) (f x))) (constraint (= (head (f x)) (+ x 7))) (check-synth) diff --git a/test/regress/regress1/sygus/max.sy b/test/regress/regress1/sygus/max.sy index 37ed848ef..f191d784f 100644 --- a/test/regress/regress1/sygus/max.sy +++ b/test/regress/regress1/sygus/max.sy @@ -1,8 +1,9 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status (set-logic LIA) (synth-fun max ((x Int) (y Int)) Int + ((Start Int) (StartBool Bool)) ((Start Int (0 1 x y (+ Start Start) (- Start Start) @@ -12,6 +13,7 @@ (<= Start Start))))) ;(synth-fun min ((x Int) (y Int)) Int +; ((Start Int) (StartBool Bool)) ; ((Start Int ((Constant Int) (Variable Int) ; (+ Start Start) ; (- Start Start) diff --git a/test/regress/regress1/sygus/parity-si-rcons.sy b/test/regress/regress1/sygus/parity-si-rcons.sy index a836c9726..850cc6610 100644 --- a/test/regress/regress1/sygus/parity-si-rcons.sy +++ b/test/regress/regress1/sygus/parity-si-rcons.sy @@ -1,5 +1,5 @@ ; EXPECT: unsat -; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status (set-logic BV) @@ -7,6 +7,7 @@ (xor (not (xor a b)) (not (xor c d)))) (synth-fun NAND ((a Bool) (b Bool) (c Bool) (d Bool)) Bool + ((Start Bool) (StartAnd Bool) (Vars Bool) (Constants Bool)) ((Start Bool ((not StartAnd) Vars Constants)) (StartAnd Bool ((and Start Start))) (Vars Bool (a b c d)) diff --git a/test/regress/regress1/sygus/re-concat.sy b/test/regress/regress1/sygus/re-concat.sy index 3449ed505..ac1172e33 100644 --- a/test/regress/regress1/sygus/re-concat.sy +++ b/test/regress/regress1/sygus/re-concat.sy @@ -1,13 +1,13 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) -(synth-fun f () RegLan ( +(synth-fun f () RegLan ((Start RegLan) (Tokens String)) ( (Start RegLan ( - (str.to.re Tokens) + (str.to_re Tokens) (re.++ Start Start))) (Tokens String ("A" "B")) )) -(constraint (str.in.re "AB" f)) +(constraint (str.in_re "AB" f)) (check-synth) diff --git a/test/regress/regress1/sygus/simple-regexp.sy b/test/regress/regress1/sygus/simple-regexp.sy index b4c248de9..b7646725d 100644 --- a/test/regress/regress1/sygus/simple-regexp.sy +++ b/test/regress/regress1/sygus/simple-regexp.sy @@ -1,30 +1,32 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status +; COMMAND-LINE: --lang=sygus2 --sygus-out=status (set-logic SLIA) -(synth-fun P ((x String)) Bool ( -(Start Bool ( - (str.in.re StartStr StartRL) +(synth-fun P ((x String)) Bool + ((Start Bool) (StartStr String) (StartStrC String) (StartRL RegLan) (StartRLi RegLan)) ( + (Start Bool ( + (str.in_re StartStr StartRL) )) -(StartStr String ( - x - (str.++ StartStr StartStr) + (StartStr String ( + x + (str.++ StartStr StartStr) + )) + (StartStrC String ( + "A" "B" "" + (str.++ StartStrC StartStrC) + )) + (StartRL RegLan ( + (re.++ StartRLi StartRLi) + (re.inter StartRL StartRL) + (re.union StartRL StartRL) + (re.* StartRLi) + )) + (StartRLi RegLan ( + (str.to_re StartStrC) + (re.inter StartRLi StartRLi) + (re.union StartRLi StartRLi) + (re.++ StartRLi StartRLi) + (re.* StartRLi) )) -(StartStrC String ( - "A" "B" "" - (str.++ StartStrC StartStrC))) -(StartRL RegLan ( -(re.++ StartRLi StartRLi) -(re.inter StartRL StartRL) -(re.union StartRL StartRL) -(re.* StartRLi) -)) -(StartRLi RegLan ( -(str.to.re StartStrC) -(re.inter StartRLi StartRLi) -(re.union StartRLi StartRLi) -(re.++ StartRLi StartRLi) -(re.* StartRLi) -)) )) (constraint (P "AAAAA")) @@ -33,5 +35,5 @@ (constraint (not (P "AB"))) (constraint (not (P "B"))) -; (str.in.re x (re.* (str.to.re "A"))) is a solution +; (str.in_re x (re.* (str.to_re "A"))) is a solution (check-synth) diff --git a/test/regress/regress1/sygus/sygus-uf-ex.sy b/test/regress/regress1/sygus/sygus-uf-ex.sy index 66880eafa..7e1cd80b3 100644 --- a/test/regress/regress1/sygus/sygus-uf-ex.sy +++ b/test/regress/regress1/sygus/sygus-uf-ex.sy @@ -1,18 +1,24 @@ ; EXPECT: unsat -; COMMAND-LINE: --sygus-out=status --uf-ho -(set-logic UFLIA) -(declare-fun uf ( Int ) Int) +; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho +(set-logic ALL) + +(declare-var uf (-> Int Int)) + (synth-fun f ((x Int) (y Int)) Bool -((Start Bool (true false - (<= IntExpr IntExpr ) - (= IntExpr IntExpr ) - (and Start Start ) - (or Start Start ) - (not Start ))) -(IntExpr Int (0 1 x y - (+ IntExpr IntExpr ) - (- IntExpr IntExpr ))))) + ((Start Bool) (IntExpr Int)) + ((Start Bool (true false + (<= IntExpr IntExpr) + (= IntExpr IntExpr) + (and Start Start) + (or Start Start) + (not Start ))) + (IntExpr Int (0 1 x y + (+ IntExpr IntExpr) + (- IntExpr IntExpr))))) + (declare-var x Int) + (constraint (f (uf x) (uf x))) (constraint (not (f 3 4))) + (check-synth) diff --git a/test/regress/regress1/test12.cvc b/test/regress/regress1/test12.cvc index 37687bee1..39ced0428 100644 --- a/test/regress/regress1/test12.cvc +++ b/test/regress/regress1/test12.cvc @@ -1,34 +1,34 @@ % COMMAND-LINE: --incremental -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: invalid -% EXPECT: valid -% EXPECT: valid -% EXPECT: valid +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: not_entailed +% EXPECT: entailed +% EXPECT: entailed +% EXPECT: entailed A: TYPE; P_1: BOOLEAN; P_2: BOOLEAN; |