diff options
Diffstat (limited to 'test/regress/regress1')
97 files changed, 126 insertions, 126 deletions
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/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/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/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; |