diff options
Diffstat (limited to 'test/regress/regress0/arith/integers')
9 files changed, 9 insertions, 9 deletions
diff --git a/test/regress/regress0/arith/integers/arith-int-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc index 265d18a84..84954a3ea 100644 --- a/test/regress/regress0/arith/integers/arith-int-014.cvc +++ b/test/regress/regress0/arith/integers/arith-int-014.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ; ASSERT (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3; diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc index d2e2639ab..8f8b01fc9 100644 --- a/test/regress/regress0/arith/integers/arith-int-015.cvc +++ b/test/regress/regress0/arith/integers/arith-int-015.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ; ASSERT (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28; diff --git a/test/regress/regress0/arith/integers/arith-int-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc index 345c90899..66f02401b 100644 --- a/test/regress/regress0/arith/integers/arith-int-021.cvc +++ b/test/regress/regress0/arith/integers/arith-int-021.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc index 01d51a226..b3d79e8ff 100644 --- a/test/regress/regress0/arith/integers/arith-int-023.cvc +++ b/test/regress/regress0/arith/integers/arith-int-023.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc index 5a11212d5..e905da9a0 100644 --- a/test/regress/regress0/arith/integers/arith-int-025.cvc +++ b/test/regress/regress0/arith/integers/arith-int-025.cvc @@ -1,4 +1,4 @@ -% EXPECT: invalid +% EXPECT: not_entailed x0, x1, x2, x3 : INT; ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3; QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc index c38231695..b6db26e86 100644 --- a/test/regress/regress0/arith/integers/arith-int-042.cvc +++ b/test/regress/regress0/arith/integers/arith-int-042.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ; ASSERT (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ; diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc index 77571e526..3fd20a0b6 100644 --- a/test/regress/regress0/arith/integers/arith-int-042.min.cvc +++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x1: INT; x0: INT; QUERY NOT (((x0 * 6) + (x1 * 32)) = 1); diff --git a/test/regress/regress0/arith/integers/arith-int-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc index 7fa2fc937..1739b3364 100644 --- a/test/regress/regress0/arith/integers/arith-int-079.cvc +++ b/test/regress/regress0/arith/integers/arith-int-079.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x0, x1, x2, x3 : INT; ASSERT (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ; ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ; diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc index d79ec94a7..ed6cb747e 100644 --- a/test/regress/regress0/arith/integers/arith-interval.cvc +++ b/test/regress/regress0/arith/integers/arith-interval.cvc @@ -1,4 +1,4 @@ -% EXPECT: valid +% EXPECT: entailed x: INT; P: INT -> BOOLEAN; |