diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-09 03:57:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-09 10:57:13 +0100 |
| commit | 59cd96a33b8f32405be2a20fc8230efc33b8dcdc (patch) | |
| tree | ad6d9b97c1a1da7026e84500f0b2ffe6081a17de /test/regress/regress1/arith | |
| parent | adc9bb5dff0c3d705b91d862d61a0c3057350688 (diff) | |
Remove obsolete regressions (#5633)
This removes benchmarks for the following reasons:
- regress1/arith/arith-int are removed since there are many similar regressions (10 from this set are already enabled)
- bitvector cvc benchmarks are removed since their *.smt2 benchmarks are enabled
- other benchmarks are removed due to features we do not plan to support
- one placeholder benchmark is removed
Diffstat (limited to 'test/regress/regress1/arith')
80 files changed, 0 insertions, 1224 deletions
diff --git a/test/regress/regress1/arith/arith-int-001.cvc b/test/regress/regress1/arith/arith-int-001.cvc deleted file mode 100644 index 3fd528c11..000000000 --- a/test/regress/regress1/arith/arith-int-001.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% 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 ; -ASSERT (-16 * x0) + (-17 * x1) + (8 * x2) + (4 * x3) > -10 ; -ASSERT (6 * x0) + (-10 * x1) + (-22 * x2) + (-22 * x3) >= 0 ; -ASSERT (18 * x0) + (0 * x1) + (27 * x2) + (7 * x3) <= -2 ; -ASSERT (-23 * x0) + (27 * x1) + (24 * x2) + (-23 * x3) > -25 ; -ASSERT (3 * x0) + (32 * x1) + (15 * x2) + (-21 * x3) >= -10 ; -ASSERT (-27 * x0) + (-16 * x1) + (21 * x2) + (-2 * x3) < 30 ; -ASSERT (-25 * x0) + (-18 * x1) + (-23 * x2) + (22 * x3) < -15 ; -ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (-26 * x3) >= 15 ; -ASSERT (-8 * x0) + (32 * x1) + (9 * x2) + (17 * x3) > -26; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-002.cvc b/test/regress/regress1/arith/arith-int-002.cvc deleted file mode 100644 index 6cc4b2c5e..000000000 --- a/test/regress/regress1/arith/arith-int-002.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% 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 ; -ASSERT (-24 * x0) + (-30 * x1) + (-14 * x2) + (13 * x3) <= 15 ; -ASSERT (-26 * x0) + (7 * x1) + (8 * x2) + (14 * x3) <= 16 ; -ASSERT (-1 * x0) + (-3 * x1) + (-19 * x2) + (26 * x3) <= -15 ; -ASSERT (31 * x0) + (19 * x1) + (-19 * x2) + (24 * x3) < -25 ; -ASSERT (8 * x0) + (-27 * x1) + (22 * x2) + (-20 * x3) < -30 ; -ASSERT (25 * x0) + (7 * x1) + (-18 * x2) + (-18 * x3) >= -31 ; -ASSERT (7 * x0) + (-22 * x1) + (-8 * x2) + (-6 * x3) >= -17 ; -ASSERT (-23 * x0) + (14 * x1) + (23 * x2) + (22 * x3) > -29 ; -ASSERT (-6 * x0) + (-6 * x1) + (-19 * x2) + (-4 * x3) > -5; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-003.cvc b/test/regress/regress1/arith/arith-int-003.cvc deleted file mode 100644 index f294babe6..000000000 --- a/test/regress/regress1/arith/arith-int-003.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% 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 ; -ASSERT (-26 * x0) + (-28 * x1) + (-23 * x2) + (0 * x3) < -14 ; -ASSERT (-12 * x0) + (16 * x1) + (26 * x2) + (-23 * x3) <= 11 ; -ASSERT (14 * x0) + (6 * x1) + (9 * x2) + (-29 * x3) > 24 ; -ASSERT (5 * x0) + (-10 * x1) + (21 * x2) + (-26 * x3) > -12 ; -ASSERT (31 * x0) + (6 * x1) + (30 * x2) + (10 * x3) <= -25 ; -ASSERT (-18 * x0) + (-25 * x1) + (-24 * x2) + (-30 * x3) >= -18 ; -ASSERT (29 * x0) + (25 * x1) + (29 * x2) + (-31 * x3) < 6 ; -ASSERT (21 * x0) + (-27 * x1) + (-28 * x2) + (-15 * x3) >= 25 ; -ASSERT (-13 * x0) + (10 * x1) + (-7 * x2) + (-10 * x3) <= -4; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-005.cvc b/test/regress/regress1/arith/arith-int-005.cvc deleted file mode 100644 index 3701d60b4..000000000 --- a/test/regress/regress1/arith/arith-int-005.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% 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 ; -ASSERT (-23 * x0) + (-26 * x1) + (4 * x2) + (-6 * x3) <= -2 ; -ASSERT (-22 * x0) + (-18 * x1) + (-23 * x2) + (5 * x3) < -32 ; -ASSERT (27 * x0) + (-12 * x1) + (-19 * x2) + (-17 * x3) <= -29 ; -ASSERT (12 * x0) + (21 * x1) + (-22 * x2) + (15 * x3) > 4 ; -ASSERT (-15 * x0) + (16 * x1) + (2 * x2) + (-14 * x3) >= -26 ; -ASSERT (4 * x0) + (4 * x1) + (-21 * x2) + (10 * x3) >= -6 ; -ASSERT (-6 * x0) + (25 * x1) + (-14 * x2) + (8 * x3) >= -31 ; -ASSERT (-23 * x0) + (2 * x1) + (-9 * x2) + (19 * x3) <= 10 ; -ASSERT (21 * x0) + (24 * x1) + (14 * x2) + (-6 * x3) <= 0; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-006.cvc b/test/regress/regress1/arith/arith-int-006.cvc deleted file mode 100644 index 53a80310a..000000000 --- a/test/regress/regress1/arith/arith-int-006.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 ; -ASSERT (24 * x0) + (-20 * x1) + (23 * x2) + (-2 * x3) = 19 ; -ASSERT (17 * x0) + (-6 * x1) + (2 * x2) + (-22 * x3) = -31 ; -ASSERT (16 * x0) + (-7 * x1) + (27 * x2) + (17 * x3) = -8; -ASSERT (-5 * x0) + (18 * x1) + (3 * x2) + (-1 * x3) <= 29 ; -ASSERT (9 * x0) + (29 * x1) + (30 * x2) + (23 * x3) >= 21 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-007.cvc b/test/regress/regress1/arith/arith-int-007.cvc deleted file mode 100644 index c0732e2b2..000000000 --- a/test/regress/regress1/arith/arith-int-007.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 ; -ASSERT (11 * x0) + (13 * x1) + (-15 * x2) + (-8 * x3) <= 18 ; -ASSERT (-21 * x0) + (0 * x1) + (32 * x2) + (7 * x3) > -31 ; -ASSERT (16 * x0) + (24 * x1) + (8 * x2) + (23 * x3) <= 16 ; -ASSERT (25 * x0) + (-11 * x1) + (-8 * x2) + (14 * x3) <= 17 ; -ASSERT (16 * x0) + (-25 * x1) + (-1 * x2) + (13 * x3) < -26; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-008.cvc b/test/regress/regress1/arith/arith-int-008.cvc deleted file mode 100644 index 1810d6f28..000000000 --- a/test/regress/regress1/arith/arith-int-008.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 ; -ASSERT (-12 * x0) + (-22 * x1) + (9 * x2) + (-20 * x3) >= 32 ; -ASSERT (24 * x0) + (-32 * x1) + (5 * x2) + (31 * x3) > 20 ; -ASSERT (-30 * x0) + (-4 * x1) + (-4 * x2) + (0 * x3) >= -20 ; -ASSERT (-10 * x0) + (18 * x1) + (17 * x2) + (20 * x3) <= 30 ; -ASSERT (12 * x0) + (-13 * x1) + (4 * x2) + (-27 * x3) > 3; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-009.cvc b/test/regress/regress1/arith/arith-int-009.cvc deleted file mode 100644 index 14b26da6c..000000000 --- a/test/regress/regress1/arith/arith-int-009.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 ; -ASSERT (11 * x0) + (15 * x1) + (-8 * x2) + (-24 * x3) = 29 ; -ASSERT (3 * x0) + (-28 * x1) + (-14 * x2) + (-18 * x3) < 5 ; -ASSERT (-18 * x0) + (-13 * x1) + (25 * x2) + (22 * x3) <= -24 ; -ASSERT (-16 * x0) + (-17 * x1) + (-27 * x2) + (4 * x3) >= -5 ; -ASSERT (21 * x0) + (13 * x1) + (20 * x2) + (-1 * x3) < 19; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-010.cvc b/test/regress/regress1/arith/arith-int-010.cvc deleted file mode 100644 index aa649ba4a..000000000 --- a/test/regress/regress1/arith/arith-int-010.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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 ; -ASSERT (-1 * x0) + (-22 * x1) + (4 * x2) + (5 * x3) = -22; -ASSERT (8 * x0) + (-8 * x1) + (18 * x2) + (-14 * x3) < -20 ; -ASSERT (22 * x0) + (27 * x1) + (6 * x2) + (-3 * x3) <= -11 ; -ASSERT (-23 * x0) + (-29 * x1) + (-27 * x2) + (13 * x3) <= 3 ; -ASSERT (8 * x0) + (0 * x1) + (28 * x2) + (0 * x3) >= -29 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-016.cvc b/test/regress/regress1/arith/arith-int-016.cvc deleted file mode 100644 index 951650461..000000000 --- a/test/regress/regress1/arith/arith-int-016.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 ; -ASSERT (-13 * x0) + (1 * x1) + (16 * x2) + (4 * x3) = -22 ; -ASSERT (17 * x0) + (7 * x1) + (32 * x2) + (19 * x3) = 16 ; -ASSERT (11 * x0) + (-8 * x1) + (-10 * x2) + (-10 * x3) <= -1 ; -ASSERT (-25 * x0) + (-18 * x1) + (-10 * x2) + (-19 * x3) <= 32 ; -ASSERT (0 * x0) + (-14 * x1) + (30 * x2) + (-5 * x3) > -13 ; -ASSERT (2 * x0) + (-17 * x1) + (-13 * x2) + (8 * x3) > 1 ; -ASSERT (-4 * x0) + (-1 * x1) + (29 * x2) + (-9 * x3) > -8 ; -ASSERT (-32 * x0) + (26 * x1) + (5 * x2) + (6 * x3) <= -1 ; -ASSERT (-26 * x0) + (3 * x1) + (22 * x2) + (27 * x3) > -2 ; -ASSERT (13 * x0) + (3 * x1) + (1 * x2) + (9 * x3) < 24 ; -ASSERT (-10 * x0) + (22 * x1) + (5 * x2) + (-5 * x3) >= -21 ; -ASSERT (-20 * x0) + (-28 * x1) + (-11 * x2) + (6 * x3) >= -17 ; -ASSERT (14 * x0) + (16 * x1) + (-15 * x2) + (17 * x3) < 27 ; -ASSERT (-23 * x0) + (-4 * x1) + (-19 * x2) + (-23 * x3) < 20 ; -ASSERT (-8 * x0) + (-5 * x1) + (-17 * x2) + (32 * x3) <= 20; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-017.cvc b/test/regress/regress1/arith/arith-int-017.cvc deleted file mode 100644 index 48287249f..000000000 --- a/test/regress/regress1/arith/arith-int-017.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 ; -ASSERT (19 * x0) + (-15 * x1) + (25 * x2) + (30 * x3) = 23 ; -ASSERT (10 * x0) + (-17 * x1) + (15 * x2) + (13 * x3) < 22 ; -ASSERT (-7 * x0) + (22 * x1) + (8 * x2) + (24 * x3) < 14 ; -ASSERT (24 * x0) + (-12 * x1) + (0 * x2) + (-25 * x3) <= -19 ; -ASSERT (-27 * x0) + (17 * x1) + (-20 * x2) + (-25 * x3) >= 11 ; -ASSERT (3 * x0) + (-12 * x1) + (-18 * x2) + (15 * x3) > -27 ; -ASSERT (-19 * x0) + (24 * x1) + (9 * x2) + (4 * x3) <= 16 ; -ASSERT (28 * x0) + (-20 * x1) + (-21 * x2) + (4 * x3) > -13 ; -ASSERT (-21 * x0) + (-23 * x1) + (-31 * x2) + (-6 * x3) < 6 ; -ASSERT (-30 * x0) + (8 * x1) + (-22 * x2) + (8 * x3) > 14 ; -ASSERT (-1 * x0) + (17 * x1) + (-22 * x2) + (-4 * x3) >= 4 ; -ASSERT (2 * x0) + (-4 * x1) + (10 * x2) + (30 * x3) < -15 ; -ASSERT (29 * x0) + (27 * x1) + (23 * x2) + (-4 * x3) < 21 ; -ASSERT (-28 * x0) + (0 * x1) + (19 * x2) + (7 * x3) <= -18 ; -ASSERT (-20 * x0) + (-7 * x1) + (26 * x2) + (-17 * x3) < 23; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-018.cvc b/test/regress/regress1/arith/arith-int-018.cvc deleted file mode 100644 index cae6fed72..000000000 --- a/test/regress/regress1/arith/arith-int-018.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 ; -ASSERT (-12 * x0) + (9 * x1) + (-22 * x2) + (11 * x3) = 11 ; -ASSERT (-27 * x0) + (8 * x1) + (-28 * x2) + (-7 * x3) = 23 ; -ASSERT (19 * x0) + (4 * x1) + (5 * x2) + (-10 * x3) >= 2 ; -ASSERT (-6 * x0) + (-20 * x1) + (30 * x2) + (20 * x3) >= 12 ; -ASSERT (19 * x0) + (26 * x1) + (-21 * x2) + (18 * x3) <= -21 ; -ASSERT (8 * x0) + (-29 * x1) + (7 * x2) + (20 * x3) >= 29 ; -ASSERT (-28 * x0) + (6 * x1) + (11 * x2) + (0 * x3) >= -4 ; -ASSERT (-20 * x0) + (-30 * x1) + (17 * x2) + (25 * x3) >= 4 ; -ASSERT (-15 * x0) + (9 * x1) + (9 * x2) + (26 * x3) > 11 ; -ASSERT (-30 * x0) + (-20 * x1) + (-20 * x2) + (14 * x3) <= -27 ; -ASSERT (-22 * x0) + (-11 * x1) + (-6 * x2) + (18 * x3) > -13 ; -ASSERT (-22 * x0) + (-25 * x1) + (22 * x2) + (-24 * x3) <= 1 ; -ASSERT (-24 * x0) + (22 * x1) + (-28 * x2) + (-14 * x3) >= 18 ; -ASSERT (17 * x0) + (31 * x1) + (-13 * x2) + (-23 * x3) < -5 ; -ASSERT (-12 * x0) + (-28 * x1) + (19 * x2) + (-21 * x3) < -27; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-019.cvc b/test/regress/regress1/arith/arith-int-019.cvc deleted file mode 100644 index a26bbac01..000000000 --- a/test/regress/regress1/arith/arith-int-019.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 ; -ASSERT (1 * x0) + (20 * x1) + (14 * x2) + (5 * x3) >= 3 ; -ASSERT (-5 * x0) + (24 * x1) + (-21 * x2) + (-13 * x3) >= -12 ; -ASSERT (9 * x0) + (-16 * x1) + (23 * x2) + (-11 * x3) > -5 ; -ASSERT (-24 * x0) + (26 * x1) + (19 * x2) + (29 * x3) > -27 ; -ASSERT (-30 * x0) + (31 * x1) + (27 * x2) + (-26 * x3) < 23 ; -ASSERT (14 * x0) + (1 * x1) + (0 * x2) + (29 * x3) > 21 ; -ASSERT (-32 * x0) + (-5 * x1) + (27 * x2) + (31 * x3) <= 23 ; -ASSERT (30 * x0) + (10 * x1) + (30 * x2) + (29 * x3) < -28 ; -ASSERT (7 * x0) + (-4 * x1) + (-25 * x2) + (0 * x3) > -28 ; -ASSERT (3 * x0) + (-19 * x1) + (11 * x2) + (-21 * x3) <= 10 ; -ASSERT (-31 * x0) + (21 * x1) + (24 * x2) + (-17 * x3) >= 21 ; -ASSERT (-20 * x0) + (19 * x1) + (6 * x2) + (5 * x3) >= -27 ; -ASSERT (-8 * x0) + (-27 * x1) + (0 * x2) + (13 * x3) >= 12 ; -ASSERT (-21 * x0) + (7 * x1) + (-26 * x2) + (19 * x3) < -10 ; -ASSERT (32 * x0) + (-26 * x1) + (-24 * x2) + (14 * x3) < 13; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-020.cvc b/test/regress/regress1/arith/arith-int-020.cvc deleted file mode 100644 index c1416b38f..000000000 --- a/test/regress/regress1/arith/arith-int-020.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% 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 ; -ASSERT (-17 * x0) + (-17 * x1) + (-22 * x2) + (30 * x3) = -5 ; -ASSERT (30 * x0) + (18 * x1) + (26 * x2) + (6 * x3) = -8 ; -ASSERT (17 * x0) + (-4 * x1) + (-16 * x2) + (-22 * x3) = 11; -ASSERT (0 * x0) + (-26 * x1) + (-15 * x2) + (12 * x3) > 7 ; -ASSERT (-30 * x0) + (4 * x1) + (-1 * x2) + (27 * x3) > 11 ; -ASSERT (23 * x0) + (12 * x1) + (11 * x2) + (-2 * x3) <= -10 ; -ASSERT (-26 * x0) + (-8 * x1) + (7 * x2) + (-18 * x3) > 1 ; -ASSERT (3 * x0) + (0 * x1) + (5 * x2) + (24 * x3) > 2 ; -ASSERT (-13 * x0) + (15 * x1) + (2 * x2) + (2 * x3) <= 17 ; -ASSERT (-24 * x0) + (21 * x1) + (-21 * x2) + (-13 * x3) >= -30 ; -ASSERT (7 * x0) + (-11 * x1) + (2 * x2) + (21 * x3) >= -24 ; -ASSERT (-15 * x0) + (-1 * x1) + (6 * x2) + (-10 * x3) <= -25 ; -ASSERT (-21 * x0) + (8 * x1) + (3 * x2) + (-5 * x3) <= 22 ; -ASSERT (-18 * x0) + (-16 * x1) + (21 * x2) + (20 * x3) >= 9 ; -ASSERT (-17 * x0) + (-10 * x1) + (-20 * x2) + (16 * x3) >= 3 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-026.cvc b/test/regress/regress1/arith/arith-int-026.cvc deleted file mode 100644 index 52f2478e0..000000000 --- a/test/regress/regress1/arith/arith-int-026.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 ; -ASSERT (0 * x0) + (-30 * x1) + (-31 * x2) + (12 * x3) = -21 ; -ASSERT (29 * x0) + (-6 * x1) + (-12 * x2) + (22 * x3) = -13; -ASSERT (-7 * x0) + (23 * x1) + (-1 * x2) + (-14 * x3) > -6 ; -ASSERT (-27 * x0) + (-31 * x1) + (25 * x2) + (-23 * x3) <= 12 ; -ASSERT (-19 * x0) + (6 * x1) + (0 * x2) + (-28 * x3) > -1 ; -ASSERT (-12 * x0) + (19 * x1) + (2 * x2) + (-4 * x3) <= 12 ; -ASSERT (10 * x0) + (-26 * x1) + (7 * x2) + (-6 * x3) < 12 ; -ASSERT (25 * x0) + (-18 * x1) + (-30 * x2) + (-9 * x3) < -2 ; -ASSERT (-9 * x0) + (-13 * x1) + (-9 * x2) + (-28 * x3) > 18 ; -ASSERT (-12 * x0) + (-28 * x1) + (-21 * x2) + (32 * x3) > 18 ; -ASSERT (-23 * x0) + (-26 * x1) + (-21 * x2) + (-24 * x3) <= 3 ; -ASSERT (-15 * x0) + (13 * x1) + (-4 * x2) + (-1 * x3) <= 0 ; -ASSERT (11 * x0) + (-30 * x1) + (3 * x2) + (-6 * x3) >= 3 ; -ASSERT (28 * x0) + (0 * x1) + (0 * x2) + (-22 * x3) >= 9 ; -ASSERT (-18 * x0) + (15 * x1) + (-27 * x2) + (31 * x3) < 5 ; -ASSERT (10 * x0) + (30 * x1) + (-28 * x2) + (27 * x3) <= -1 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-027.cvc b/test/regress/regress1/arith/arith-int-027.cvc deleted file mode 100644 index 6c38642d2..000000000 --- a/test/regress/regress1/arith/arith-int-027.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 ; -ASSERT (-12 * x0) + (-3 * x1) + (-19 * x2) + (4 * x3) = -21 ; -ASSERT (-3 * x0) + (10 * x1) + (-6 * x2) + (-31 * x3) = 21 ; -ASSERT (10 * x0) + (-14 * x1) + (-12 * x2) + (8 * x3) = 5 ; -ASSERT (-4 * x0) + (15 * x1) + (29 * x2) + (2 * x3) = -32 ; -ASSERT (-14 * x0) + (-12 * x1) + (16 * x2) + (-14 * x3) = -8 ; -ASSERT (-31 * x0) + (14 * x1) + (30 * x2) + (-19 * x3) < -20 ; -ASSERT (-5 * x0) + (9 * x1) + (11 * x2) + (-32 * x3) < 3 ; -ASSERT (27 * x0) + (-6 * x1) + (0 * x2) + (30 * x3) <= -20 ; -ASSERT (-15 * x0) + (-13 * x1) + (-21 * x2) + (-5 * x3) > -8 ; -ASSERT (19 * x0) + (31 * x1) + (-16 * x2) + (-8 * x3) > -15 ; -ASSERT (9 * x0) + (-9 * x1) + (-4 * x2) + (-16 * x3) < 21 ; -ASSERT (24 * x0) + (4 * x1) + (28 * x2) + (-14 * x3) >= -1 ; -ASSERT (5 * x0) + (23 * x1) + (-22 * x2) + (-28 * x3) >= -21 ; -ASSERT (-31 * x0) + (14 * x1) + (14 * x2) + (-9 * x3) > -32 ; -ASSERT (25 * x0) + (-18 * x1) + (21 * x2) + (-17 * x3) < -20 ; -ASSERT (1 * x0) + (-29 * x1) + (11 * x2) + (-24 * x3) >= -20; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-028.cvc b/test/regress/regress1/arith/arith-int-028.cvc deleted file mode 100644 index 7e8b78893..000000000 --- a/test/regress/regress1/arith/arith-int-028.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 ; -ASSERT (31 * x0) + (28 * x1) + (-20 * x2) + (15 * x3) = -30; -ASSERT (15 * x0) + (-16 * x1) + (29 * x2) + (-2 * x3) >= -6 ; -ASSERT (-29 * x0) + (-17 * x1) + (-7 * x2) + (11 * x3) < 26 ; -ASSERT (-4 * x0) + (14 * x1) + (-29 * x2) + (-7 * x3) >= 28 ; -ASSERT (-29 * x0) + (-25 * x1) + (9 * x2) + (-17 * x3) <= -25 ; -ASSERT (10 * x0) + (-25 * x1) + (28 * x2) + (8 * x3) > 6 ; -ASSERT (10 * x0) + (17 * x1) + (-1 * x2) + (21 * x3) > 24 ; -ASSERT (-19 * x0) + (-29 * x1) + (-26 * x2) + (-7 * x3) <= -11 ; -ASSERT (30 * x0) + (-7 * x1) + (-8 * x2) + (6 * x3) >= -32 ; -ASSERT (-3 * x0) + (24 * x1) + (30 * x2) + (-30 * x3) >= 19 ; -ASSERT (-9 * x0) + (5 * x1) + (17 * x2) + (-24 * x3) < -22 ; -ASSERT (11 * x0) + (-16 * x1) + (-1 * x2) + (26 * x3) >= 1 ; -ASSERT (-13 * x0) + (5 * x1) + (19 * x2) + (4 * x3) >= 27 ; -ASSERT (23 * x0) + (4 * x1) + (30 * x2) + (-28 * x3) > 13 ; -ASSERT (-8 * x0) + (-24 * x1) + (0 * x2) + (22 * x3) < -6 ; -ASSERT (-1 * x0) + (1 * x1) + (-30 * x2) + (12 * x3) >= -26 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-029.cvc b/test/regress/regress1/arith/arith-int-029.cvc deleted file mode 100644 index ba49219d8..000000000 --- a/test/regress/regress1/arith/arith-int-029.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 ; -ASSERT (-19 * x0) + (29 * x1) + (27 * x2) + (-8 * x3) = -4 ; -ASSERT (-28 * x0) + (-15 * x1) + (-20 * x2) + (-1 * x3) = -2 ; -ASSERT (-2 * x0) + (2 * x1) + (3 * x2) + (-4 * x3) = 16 ; -ASSERT (31 * x0) + (22 * x1) + (15 * x2) + (28 * x3) = -19 ; -ASSERT (-32 * x0) + (2 * x1) + (-8 * x2) + (6 * x3) <= -21 ; -ASSERT (-10 * x0) + (23 * x1) + (-9 * x2) + (-26 * x3) < -7 ; -ASSERT (-11 * x0) + (-13 * x1) + (-17 * x2) + (-19 * x3) >= -11 ; -ASSERT (20 * x0) + (11 * x1) + (-11 * x2) + (-7 * x3) <= 14 ; -ASSERT (17 * x0) + (0 * x1) + (-27 * x2) + (-32 * x3) > -1 ; -ASSERT (17 * x0) + (-7 * x1) + (18 * x2) + (-29 * x3) > -19 ; -ASSERT (12 * x0) + (-14 * x1) + (27 * x2) + (5 * x3) <= 23 ; -ASSERT (-2 * x0) + (-6 * x1) + (-6 * x2) + (19 * x3) < -5 ; -ASSERT (-3 * x0) + (-10 * x1) + (-30 * x2) + (18 * x3) >= -27 ; -ASSERT (-18 * x0) + (-25 * x1) + (3 * x2) + (2 * x3) < -25 ; -ASSERT (-19 * x0) + (16 * x1) + (-11 * x2) + (-26 * x3) >= -24 ; -ASSERT (-2 * x0) + (21 * x1) + (25 * x2) + (28 * x3) > 10; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-030.cvc b/test/regress/regress1/arith/arith-int-030.cvc deleted file mode 100644 index a6348b107..000000000 --- a/test/regress/regress1/arith/arith-int-030.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% 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 ; -ASSERT (8 * x0) + (-24 * x1) + (20 * x2) + (23 * x3) = -23 ; -ASSERT (-2 * x0) + (26 * x1) + (4 * x2) + (31 * x3) < 31 ; -ASSERT (23 * x0) + (14 * x1) + (-29 * x2) + (-11 * x3) > 14 ; -ASSERT (-19 * x0) + (-32 * x1) + (11 * x2) + (31 * x3) < -4 ; -ASSERT (3 * x0) + (13 * x1) + (-19 * x2) + (26 * x3) >= -20 ; -ASSERT (-6 * x0) + (4 * x1) + (-17 * x2) + (-31 * x3) <= 32 ; -ASSERT (-13 * x0) + (32 * x1) + (-18 * x2) + (7 * x3) < -27 ; -ASSERT (-19 * x0) + (6 * x1) + (-28 * x2) + (-15 * x3) >= 30 ; -ASSERT (30 * x0) + (-24 * x1) + (-10 * x2) + (-4 * x3) >= -9 ; -ASSERT (-4 * x0) + (4 * x1) + (-27 * x2) + (-17 * x3) < 12 ; -ASSERT (-21 * x0) + (13 * x1) + (31 * x2) + (4 * x3) >= -16 ; -ASSERT (-11 * x0) + (30 * x1) + (-20 * x2) + (21 * x3) <= 9 ; -ASSERT (-12 * x0) + (23 * x1) + (2 * x2) + (12 * x3) <= 18 ; -ASSERT (30 * x0) + (8 * x1) + (4 * x2) + (-5 * x3) <= -24 ; -ASSERT (12 * x0) + (22 * x1) + (9 * x2) + (30 * x3) >= -3 ; -ASSERT (10 * x0) + (15 * x1) + (25 * x2) + (-5 * x3) <= 4; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-031.cvc b/test/regress/regress1/arith/arith-int-031.cvc deleted file mode 100644 index 056ab622e..000000000 --- a/test/regress/regress1/arith/arith-int-031.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 ; -ASSERT (0 * x0) + (22 * x1) + (-11 * x2) + (-22 * x3) <= 26 ; -ASSERT (17 * x0) + (-11 * x1) + (32 * x2) + (8 * x3) < 20 ; -ASSERT (-30 * x0) + (24 * x1) + (-30 * x2) + (-12 * x3) >= 19 ; -ASSERT (-27 * x0) + (5 * x1) + (31 * x2) + (-12 * x3) <= -24 ; -ASSERT (-12 * x0) + (-23 * x1) + (-27 * x2) + (29 * x3) >= 13 ; -ASSERT (23 * x0) + (-21 * x1) + (24 * x2) + (-17 * x3) >= -20 ; -ASSERT (-30 * x0) + (-27 * x1) + (-21 * x2) + (-11 * x3) < -24 ; -ASSERT (31 * x0) + (-14 * x1) + (-3 * x2) + (-9 * x3) >= 13 ; -ASSERT (8 * x0) + (-2 * x1) + (-13 * x2) + (23 * x3) < 31 ; -ASSERT (-1 * x0) + (9 * x1) + (-29 * x2) + (17 * x3) >= -7 ; -ASSERT (11 * x0) + (-8 * x1) + (-29 * x2) + (-25 * x3) >= -5 ; -ASSERT (19 * x0) + (-32 * x1) + (27 * x2) + (17 * x3) > 17 ; -ASSERT (23 * x0) + (-1 * x1) + (-9 * x2) + (-12 * x3) < -25 ; -ASSERT (16 * x0) + (-22 * x1) + (3 * x2) + (30 * x3) >= 11; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-032.cvc b/test/regress/regress1/arith/arith-int-032.cvc deleted file mode 100644 index 08c29108e..000000000 --- a/test/regress/regress1/arith/arith-int-032.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 ; -ASSERT (-15 * x0) + (-4 * x1) + (-28 * x2) + (-25 * x3) = 13 ; -ASSERT (17 * x0) + (-29 * x1) + (19 * x2) + (-32 * x3) = 26 ; -ASSERT (20 * x0) + (-29 * x1) + (-32 * x2) + (28 * x3) = -12 ; -ASSERT (17 * x0) + (18 * x1) + (-18 * x2) + (28 * x3) <= 21 ; -ASSERT (-28 * x0) + (-17 * x1) + (-15 * x2) + (30 * x3) > -19 ; -ASSERT (-6 * x0) + (-25 * x1) + (-22 * x2) + (-13 * x3) < -8 ; -ASSERT (12 * x0) + (8 * x1) + (15 * x2) + (-7 * x3) >= 12 ; -ASSERT (14 * x0) + (6 * x1) + (3 * x2) + (25 * x3) > 3 ; -ASSERT (31 * x0) + (5 * x1) + (26 * x2) + (-1 * x3) < -13 ; -ASSERT (31 * x0) + (-27 * x1) + (15 * x2) + (-16 * x3) >= 11 ; -ASSERT (20 * x0) + (-20 * x1) + (25 * x2) + (18 * x3) > 18 ; -ASSERT (-2 * x0) + (-30 * x1) + (25 * x2) + (-9 * x3) < -9 ; -ASSERT (29 * x0) + (-22 * x1) + (-18 * x2) + (-25 * x3) < -2 ; -ASSERT (-12 * x0) + (9 * x1) + (17 * x2) + (-16 * x3) > 3; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-033.cvc b/test/regress/regress1/arith/arith-int-033.cvc deleted file mode 100644 index 8259a7725..000000000 --- a/test/regress/regress1/arith/arith-int-033.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 ; -ASSERT (-28 * x0) + (31 * x1) + (32 * x2) + (-11 * x3) = 0 ; -ASSERT (-20 * x0) + (-11 * x1) + (-27 * x2) + (-6 * x3) = -6 ; -ASSERT (-7 * x0) + (-7 * x1) + (17 * x2) + (-25 * x3) <= -15 ; -ASSERT (8 * x0) + (28 * x1) + (8 * x2) + (7 * x3) > -28 ; -ASSERT (25 * x0) + (7 * x1) + (-17 * x2) + (-28 * x3) > 5 ; -ASSERT (-19 * x0) + (0 * x1) + (-20 * x2) + (0 * x3) <= 20 ; -ASSERT (6 * x0) + (2 * x1) + (29 * x2) + (-19 * x3) <= -3 ; -ASSERT (-9 * x0) + (-1 * x1) + (-18 * x2) + (32 * x3) > 11 ; -ASSERT (2 * x0) + (21 * x1) + (0 * x2) + (19 * x3) >= 13 ; -ASSERT (-26 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) < -24 ; -ASSERT (-23 * x0) + (22 * x1) + (12 * x2) + (19 * x3) < -27 ; -ASSERT (-25 * x0) + (-31 * x1) + (28 * x2) + (14 * x3) < 14 ; -ASSERT (-29 * x0) + (1 * x1) + (26 * x2) + (-27 * x3) < -14 ; -ASSERT (23 * x0) + (26 * x1) + (-5 * x2) + (6 * x3) <= -19; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-034.cvc b/test/regress/regress1/arith/arith-int-034.cvc deleted file mode 100644 index 2b5ae4f4f..000000000 --- a/test/regress/regress1/arith/arith-int-034.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 ; -ASSERT (14 * x0) + (11 * x1) + (17 * x2) + (12 * x3) = -5 ; -ASSERT (-29 * x0) + (-29 * x1) + (-16 * x2) + (14 * x3) = 10 ; -ASSERT (30 * x0) + (13 * x1) + (10 * x2) + (24 * x3) = 3 ; -ASSERT (-20 * x0) + (29 * x1) + (28 * x2) + (27 * x3) < -21 ; -ASSERT (-31 * x0) + (17 * x1) + (14 * x2) + (-14 * x3) <= 14 ; -ASSERT (-23 * x0) + (19 * x1) + (28 * x2) + (-2 * x3) > -28 ; -ASSERT (-23 * x0) + (23 * x1) + (19 * x2) + (25 * x3) > 13 ; -ASSERT (-32 * x0) + (8 * x1) + (-24 * x2) + (10 * x3) >= -5 ; -ASSERT (-30 * x0) + (1 * x1) + (-22 * x2) + (12 * x3) >= -30 ; -ASSERT (8 * x0) + (28 * x1) + (17 * x2) + (-7 * x3) < -20 ; -ASSERT (-28 * x0) + (-8 * x1) + (27 * x2) + (25 * x3) >= 7 ; -ASSERT (-15 * x0) + (26 * x1) + (9 * x2) + (15 * x3) > -12 ; -ASSERT (-3 * x0) + (15 * x1) + (-6 * x2) + (-31 * x3) < -24 ; -ASSERT (-26 * x0) + (22 * x1) + (16 * x2) + (30 * x3) <= -2; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-035.cvc b/test/regress/regress1/arith/arith-int-035.cvc deleted file mode 100644 index 1bad259e2..000000000 --- a/test/regress/regress1/arith/arith-int-035.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% 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 ; -ASSERT (8 * x0) + (23 * x1) + (26 * x2) + (-1 * x3) >= -6 ; -ASSERT (-7 * x0) + (4 * x1) + (9 * x2) + (-30 * x3) > -26 ; -ASSERT (-14 * x0) + (-31 * x1) + (-18 * x2) + (-5 * x3) <= 6 ; -ASSERT (15 * x0) + (26 * x1) + (3 * x2) + (-24 * x3) >= 6 ; -ASSERT (13 * x0) + (0 * x1) + (25 * x2) + (-27 * x3) <= -13 ; -ASSERT (11 * x0) + (20 * x1) + (-28 * x2) + (8 * x3) < 0 ; -ASSERT (-10 * x0) + (13 * x1) + (20 * x2) + (19 * x3) >= 29 ; -ASSERT (12 * x0) + (-9 * x1) + (-16 * x2) + (26 * x3) >= -11 ; -ASSERT (-2 * x0) + (32 * x1) + (-6 * x2) + (21 * x3) > -31 ; -ASSERT (-1 * x0) + (-22 * x1) + (-22 * x2) + (-5 * x3) > 29 ; -ASSERT (-8 * x0) + (19 * x1) + (18 * x2) + (32 * x3) >= 12 ; -ASSERT (26 * x0) + (16 * x1) + (-25 * x2) + (29 * x3) < 29 ; -ASSERT (1 * x0) + (-18 * x1) + (11 * x2) + (-10 * x3) > 10 ; -ASSERT (-21 * x0) + (5 * x1) + (-2 * x2) + (-28 * x3) <= -5; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-036.cvc b/test/regress/regress1/arith/arith-int-036.cvc deleted file mode 100644 index 0eb783815..000000000 --- a/test/regress/regress1/arith/arith-int-036.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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 ; -ASSERT (15 * x0) + (5 * x1) + (5 * x2) + (19 * x3) = -29 ; -ASSERT (-9 * x0) + (-23 * x1) + (7 * x2) + (-21 * x3) = 28 ; -ASSERT (-24 * x0) + (-22 * x1) + (30 * x2) + (-31 * x3) = -24 ; -ASSERT (-29 * x0) + (-21 * x1) + (26 * x2) + (-13 * x3) < -12 ; -ASSERT (31 * x0) + (6 * x1) + (-23 * x2) + (30 * x3) < -3 ; -ASSERT (21 * x0) + (-7 * x1) + (-4 * x2) + (-25 * x3) <= -17 ; -ASSERT (4 * x0) + (24 * x1) + (21 * x2) + (8 * x3) <= 19 ; -ASSERT (19 * x0) + (30 * x1) + (14 * x2) + (-23 * x3) > 21 ; -ASSERT (30 * x0) + (3 * x1) + (-28 * x2) + (25 * x3) <= -27 ; -ASSERT (0 * x0) + (-17 * x1) + (-9 * x2) + (-8 * x3) <= 31 ; -ASSERT (-6 * x0) + (-23 * x1) + (21 * x2) + (18 * x3) >= 31; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-037.cvc b/test/regress/regress1/arith/arith-int-037.cvc deleted file mode 100644 index c3ed60011..000000000 --- a/test/regress/regress1/arith/arith-int-037.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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 ; -ASSERT (-10 * x0) + (7 * x1) + (-23 * x2) + (18 * x3) <= -16 ; -ASSERT (-12 * x0) + (7 * x1) + (-16 * x2) + (16 * x3) > -31 ; -ASSERT (10 * x0) + (11 * x1) + (-17 * x2) + (19 * x3) <= 9 ; -ASSERT (-1 * x0) + (-8 * x1) + (-31 * x2) + (16 * x3) > 20 ; -ASSERT (-9 * x0) + (18 * x1) + (9 * x2) + (-14 * x3) <= -8 ; -ASSERT (-9 * x0) + (27 * x1) + (-22 * x2) + (-16 * x3) > 27 ; -ASSERT (-24 * x0) + (-25 * x1) + (-28 * x2) + (29 * x3) <= -9 ; -ASSERT (4 * x0) + (13 * x1) + (27 * x2) + (-5 * x3) >= -22 ; -ASSERT (-20 * x0) + (-14 * x1) + (21 * x2) + (-28 * x3) <= 17 ; -ASSERT (18 * x0) + (-32 * x1) + (-23 * x2) + (-9 * x3) <= -21 ; -ASSERT (19 * x0) + (-9 * x1) + (18 * x2) + (-9 * x3) <= -19; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-038.cvc b/test/regress/regress1/arith/arith-int-038.cvc deleted file mode 100644 index 52ac2b1e3..000000000 --- a/test/regress/regress1/arith/arith-int-038.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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 ; -ASSERT (-16 * x0) + (-4 * x1) + (-2 * x2) + (-1 * x3) >= -28 ; -ASSERT (4 * x0) + (-26 * x1) + (2 * x2) + (-8 * x3) > 7 ; -ASSERT (-17 * x0) + (-6 * x1) + (11 * x2) + (-9 * x3) > -27 ; -ASSERT (-25 * x0) + (13 * x1) + (-29 * x2) + (15 * x3) > 2 ; -ASSERT (32 * x0) + (-10 * x1) + (15 * x2) + (-25 * x3) < -25 ; -ASSERT (-16 * x0) + (-26 * x1) + (16 * x2) + (3 * x3) > -26 ; -ASSERT (-14 * x0) + (13 * x1) + (4 * x2) + (-24 * x3) >= -14 ; -ASSERT (-5 * x0) + (-21 * x1) + (-7 * x2) + (10 * x3) < 0 ; -ASSERT (0 * x0) + (25 * x1) + (31 * x2) + (30 * x3) <= -25 ; -ASSERT (-1 * x0) + (2 * x1) + (26 * x2) + (4 * x3) <= 4 ; -ASSERT (14 * x0) + (23 * x1) + (18 * x2) + (-18 * x3) > 19; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-039.cvc b/test/regress/regress1/arith/arith-int-039.cvc deleted file mode 100644 index cecb7f085..000000000 --- a/test/regress/regress1/arith/arith-int-039.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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 ; -ASSERT (12 * x0) + (18 * x1) + (29 * x2) + (17 * x3) = 0 ; -ASSERT (-8 * x0) + (-10 * x1) + (-27 * x2) + (30 * x3) = 32 ; -ASSERT (-21 * x0) + (-2 * x1) + (20 * x2) + (-7 * x3) <= -27 ; -ASSERT (-7 * x0) + (-22 * x1) + (8 * x2) + (20 * x3) > -20 ; -ASSERT (-10 * x0) + (1 * x1) + (21 * x2) + (-6 * x3) > 10 ; -ASSERT (-21 * x0) + (-24 * x1) + (-15 * x2) + (4 * x3) <= 11 ; -ASSERT (-32 * x0) + (10 * x1) + (-21 * x2) + (-17 * x3) <= 5 ; -ASSERT (7 * x0) + (-19 * x1) + (28 * x2) + (27 * x3) <= 14 ; -ASSERT (-32 * x0) + (5 * x1) + (26 * x2) + (-23 * x3) < -23 ; -ASSERT (-28 * x0) + (5 * x1) + (22 * x2) + (25 * x3) < 6 ; -ASSERT (4 * x0) + (17 * x1) + (11 * x2) + (26 * x3) >= 20; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-040.cvc b/test/regress/regress1/arith/arith-int-040.cvc deleted file mode 100644 index f2dff7796..000000000 --- a/test/regress/regress1/arith/arith-int-040.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% 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 ; -ASSERT (18 * x0) + (15 * x1) + (-27 * x2) + (8 * x3) > -11 ; -ASSERT (-14 * x0) + (4 * x1) + (27 * x2) + (-9 * x3) < -13 ; -ASSERT (24 * x0) + (11 * x1) + (17 * x2) + (-15 * x3) > 5 ; -ASSERT (-28 * x0) + (-1 * x1) + (10 * x2) + (-12 * x3) > -14 ; -ASSERT (-11 * x0) + (-4 * x1) + (7 * x2) + (-32 * x3) >= 31 ; -ASSERT (18 * x0) + (32 * x1) + (-24 * x2) + (-19 * x3) <= -6 ; -ASSERT (-15 * x0) + (23 * x1) + (-19 * x2) + (-12 * x3) < 2 ; -ASSERT (-21 * x0) + (-8 * x1) + (-30 * x2) + (31 * x3) >= -29 ; -ASSERT (5 * x0) + (-24 * x1) + (-21 * x2) + (-10 * x3) >= -8 ; -ASSERT (-31 * x0) + (-26 * x1) + (13 * x2) + (-7 * x3) <= -32 ; -ASSERT (-18 * x0) + (-11 * x1) + (9 * x2) + (6 * x3) >= 8; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-041.cvc b/test/regress/regress1/arith/arith-int-041.cvc deleted file mode 100644 index 9df03a9bd..000000000 --- a/test/regress/regress1/arith/arith-int-041.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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 ; -ASSERT (-16 * x0) + (-11 * x1) + (-32 * x2) + (-18 * x3) > -29 ; -ASSERT (32 * x0) + (-2 * x1) + (27 * x2) + (0 * x3) >= -1 ; -ASSERT (12 * x0) + (-17 * x1) + (21 * x2) + (-3 * x3) <= 1 ; -ASSERT (-26 * x0) + (29 * x1) + (-13 * x2) + (15 * x3) <= 2; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-043.cvc b/test/regress/regress1/arith/arith-int-043.cvc deleted file mode 100644 index 7a2d6d6af..000000000 --- a/test/regress/regress1/arith/arith-int-043.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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 ; -ASSERT (2 * x0) + (-22 * x1) + (-30 * x2) + (-9 * x3) >= 17 ; -ASSERT (21 * x0) + (5 * x1) + (-13 * x2) + (0 * x3) <= 18 ; -ASSERT (9 * x0) + (-5 * x1) + (30 * x2) + (17 * x3) > -12 ; -ASSERT (-2 * x0) + (-27 * x1) + (-5 * x2) + (-23 * x3) < 24; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-044.cvc b/test/regress/regress1/arith/arith-int-044.cvc deleted file mode 100644 index 649532a4b..000000000 --- a/test/regress/regress1/arith/arith-int-044.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% 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; -ASSERT (-25 * x0) + (-16 * x1) + (17 * x2) + (26 * x3) < 23 ; -ASSERT (-27 * x0) + (9 * x1) + (7 * x2) + (-24 * x3) < -27 ; -ASSERT (14 * x0) + (-27 * x1) + (-10 * x2) + (16 * x3) >= -23 ; -ASSERT (14 * x0) + (-27 * x1) + (-3 * x2) + (2 * x3) > -9 ; -ASSERT (-19 * x0) + (-9 * x1) + (-3 * x2) + (29 * x3) <= 5 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-045.cvc b/test/regress/regress1/arith/arith-int-045.cvc deleted file mode 100644 index 2c552c915..000000000 --- a/test/regress/regress1/arith/arith-int-045.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% 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 ; -ASSERT (30 * x0) + (6 * x1) + (-17 * x2) + (-6 * x3) > 8 ; -ASSERT (28 * x0) + (-17 * x1) + (26 * x2) + (-1 * x3) >= 17 ; -ASSERT (2 * x0) + (-32 * x1) + (30 * x2) + (10 * x3) < -23 ; -ASSERT (22 * x0) + (-18 * x1) + (7 * x2) + (28 * x3) < -26; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-046.cvc b/test/regress/regress1/arith/arith-int-046.cvc deleted file mode 100644 index acf4dc9a9..000000000 --- a/test/regress/regress1/arith/arith-int-046.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% 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 ; -ASSERT (-11 * x0) + (28 * x1) + (-20 * x2) + (-2 * x3) >= 31; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-049.cvc b/test/regress/regress1/arith/arith-int-049.cvc deleted file mode 100644 index 72e3b7f31..000000000 --- a/test/regress/regress1/arith/arith-int-049.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% 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 ; -ASSERT (14 * x0) + (-6 * x1) + (28 * x2) + (-22 * x3) < -16; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-051.cvc b/test/regress/regress1/arith/arith-int-051.cvc deleted file mode 100644 index 68654a7df..000000000 --- a/test/regress/regress1/arith/arith-int-051.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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 ; -ASSERT (-9 * x0) + (12 * x1) + (23 * x2) + (-24 * x3) >= -30 ; -ASSERT (-13 * x0) + (-3 * x1) + (-15 * x2) + (32 * x3) <= 26 ; -ASSERT (-27 * x0) + (9 * x1) + (-21 * x2) + (-5 * x3) < -9 ; -ASSERT (22 * x0) + (24 * x1) + (-10 * x2) + (-6 * x3) > -1 ; -ASSERT (20 * x0) + (-24 * x1) + (29 * x2) + (-21 * x3) <= 29 ; -ASSERT (25 * x0) + (11 * x1) + (8 * x2) + (-5 * x3) < -29 ; -ASSERT (-12 * x0) + (24 * x1) + (4 * x2) + (27 * x3) < 31; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-052.cvc b/test/regress/regress1/arith/arith-int-052.cvc deleted file mode 100644 index 9c9433ede..000000000 --- a/test/regress/regress1/arith/arith-int-052.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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 ; -ASSERT (29 * x0) + (-8 * x1) + (22 * x2) + (20 * x3) < 14 ; -ASSERT (31 * x0) + (-16 * x1) + (-17 * x2) + (-21 * x3) >= 32 ; -ASSERT (-24 * x0) + (-29 * x1) + (9 * x2) + (14 * x3) <= -4 ; -ASSERT (13 * x0) + (13 * x1) + (14 * x2) + (5 * x3) <= 25 ; -ASSERT (5 * x0) + (12 * x1) + (-5 * x2) + (-9 * x3) >= -28 ; -ASSERT (27 * x0) + (19 * x1) + (6 * x2) + (25 * x3) >= -12 ; -ASSERT (24 * x0) + (-26 * x1) + (2 * x2) + (0 * x3) >= -25; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-053.cvc b/test/regress/regress1/arith/arith-int-053.cvc deleted file mode 100644 index 544d53fb9..000000000 --- a/test/regress/regress1/arith/arith-int-053.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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; -ASSERT (28 * x0) + (30 * x1) + (26 * x2) + (2 * x3) < 8 ; -ASSERT (17 * x0) + (-11 * x1) + (6 * x2) + (8 * x3) > 11 ; -ASSERT (20 * x0) + (-14 * x1) + (16 * x2) + (-3 * x3) < 9 ; -ASSERT (-11 * x0) + (2 * x1) + (4 * x2) + (-4 * x3) < -21 ; -ASSERT (25 * x0) + (6 * x1) + (-22 * x2) + (8 * x3) <= 7 ; -ASSERT (-8 * x0) + (9 * x1) + (-13 * x2) + (27 * x3) >= 0 ; -ASSERT (-16 * x0) + (-8 * x1) + (23 * x2) + (25 * x3) >= -13 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-054.cvc b/test/regress/regress1/arith/arith-int-054.cvc deleted file mode 100644 index 5b4181a11..000000000 --- a/test/regress/regress1/arith/arith-int-054.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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 ; -ASSERT (19 * x0) + (-30 * x1) + (8 * x2) + (-4 * x3) = -17 ; -ASSERT (-10 * x0) + (26 * x1) + (11 * x2) + (-31 * x3) = -26; -ASSERT (-22 * x0) + (15 * x1) + (14 * x2) + (3 * x3) <= -3 ; -ASSERT (-15 * x0) + (7 * x1) + (29 * x2) + (16 * x3) >= -6 ; -ASSERT (-20 * x0) + (20 * x1) + (31 * x2) + (-24 * x3) <= 14 ; -ASSERT (2 * x0) + (31 * x1) + (15 * x2) + (-1 * x3) >= -6 ; -ASSERT (-30 * x0) + (-11 * x1) + (26 * x2) + (6 * x3) >= -30 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-055.cvc b/test/regress/regress1/arith/arith-int-055.cvc deleted file mode 100644 index fdfa45848..000000000 --- a/test/regress/regress1/arith/arith-int-055.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% 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 ; -ASSERT (-26 * x0) + (-7 * x1) + (-25 * x2) + (-19 * x3) < -4 ; -ASSERT (4 * x0) + (14 * x1) + (-16 * x2) + (-32 * x3) >= -16 ; -ASSERT (10 * x0) + (-9 * x1) + (20 * x2) + (-27 * x3) <= 31 ; -ASSERT (29 * x0) + (16 * x1) + (25 * x2) + (-1 * x3) < -26 ; -ASSERT (-29 * x0) + (1 * x1) + (11 * x2) + (32 * x3) < 12 ; -ASSERT (-4 * x0) + (-22 * x1) + (0 * x2) + (-29 * x3) < 31 ; -ASSERT (12 * x0) + (-8 * x1) + (-17 * x2) + (-8 * x3) > 8; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-056.cvc b/test/regress/regress1/arith/arith-int-056.cvc deleted file mode 100644 index 394b3dd4e..000000000 --- a/test/regress/regress1/arith/arith-int-056.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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 ; -ASSERT (3 * x0) + (-32 * x1) + (-23 * x2) + (13 * x3) = 16 ; -ASSERT (25 * x0) + (-14 * x1) + (-17 * x2) + (16 * x3) <= 24 ; -ASSERT (1 * x0) + (-21 * x1) + (2 * x2) + (2 * x3) >= 15 ; -ASSERT (24 * x0) + (9 * x1) + (23 * x2) + (-2 * x3) >= -26 ; -%%ASSERT (-25 * x0) + (26 * x1) + (-3 * x2) + (-26 * x3) >= -20 ; -%%ASSERT (4 * x0) + (23 * x1) + (-24 * x2) + (7 * x3) <= -18 ; -%%ASSERT (-16 * x0) + (-24 * x1) + (26 * x2) + (1 * x3) > 15 ; -%%%%ASSERT (1 * x0) + (9 * x1) + (-18 * x2) + (11 * x3) > -3 ; -%%ASSERT (-9 * x0) + (20 * x1) + (15 * x2) + (4 * x3) < -17 ; -%%ASSERT (25 * x0) + (-22 * x1) + (-26 * x2) + (-21 * x3) > 17; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-057.cvc b/test/regress/regress1/arith/arith-int-057.cvc deleted file mode 100644 index 252601514..000000000 --- a/test/regress/regress1/arith/arith-int-057.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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; -ASSERT (2 * x0) + (22 * x1) + (-13 * x2) + (16 * x3) <= 17 ; -ASSERT (18 * x0) + (18 * x1) + (15 * x2) + (-17 * x3) < -13 ; -ASSERT (-24 * x0) + (-8 * x1) + (31 * x2) + (-25 * x3) > 23 ; -ASSERT (-13 * x0) + (-22 * x1) + (11 * x2) + (28 * x3) >= -6 ; -ASSERT (20 * x0) + (-26 * x1) + (-20 * x2) + (-7 * x3) < -5 ; -ASSERT (-23 * x0) + (8 * x1) + (28 * x2) + (17 * x3) > 23 ; -ASSERT (32 * x0) + (31 * x1) + (-26 * x2) + (29 * x3) <= -1 ; -ASSERT (-2 * x0) + (-11 * x1) + (15 * x2) + (17 * x3) > -27 ; -ASSERT (-13 * x0) + (-30 * x1) + (-25 * x2) + (-18 * x3) <= 24 ; -ASSERT (23 * x0) + (-4 * x1) + (26 * x2) + (32 * x3) >= 23 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-058.cvc b/test/regress/regress1/arith/arith-int-058.cvc deleted file mode 100644 index 7e2a04d45..000000000 --- a/test/regress/regress1/arith/arith-int-058.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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 ; -ASSERT (-17 * x0) + (31 * x1) + (-11 * x2) + (-29 * x3) = -2 ; -ASSERT (18 * x0) + (11 * x1) + (13 * x2) + (-16 * x3) >= 5 ; -ASSERT (-28 * x0) + (-30 * x1) + (13 * x2) + (-20 * x3) <= -19 ; -ASSERT (-10 * x0) + (-20 * x1) + (-13 * x2) + (-4 * x3) < 3 ; -ASSERT (-30 * x0) + (-5 * x1) + (-15 * x2) + (-1 * x3) > 19 ; -ASSERT (-8 * x0) + (28 * x1) + (17 * x2) + (23 * x3) <= 30 ; -ASSERT (-28 * x0) + (-16 * x1) + (-19 * x2) + (-23 * x3) >= 9 ; -ASSERT (-8 * x0) + (-15 * x1) + (-19 * x2) + (29 * x3) > -28 ; -ASSERT (-27 * x0) + (-12 * x1) + (-2 * x2) + (-29 * x3) >= -5 ; -ASSERT (32 * x0) + (-16 * x1) + (29 * x2) + (-12 * x3) < 26; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-059.cvc b/test/regress/regress1/arith/arith-int-059.cvc deleted file mode 100644 index 87773679e..000000000 --- a/test/regress/regress1/arith/arith-int-059.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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 ; -ASSERT (-6 * x0) + (-21 * x1) + (-11 * x2) + (-10 * x3) = 11 ; -ASSERT (22 * x0) + (-7 * x1) + (2 * x2) + (-16 * x3) = 16; -ASSERT (15 * x0) + (-14 * x1) + (29 * x2) + (24 * x3) >= 14 ; -ASSERT (-26 * x0) + (-6 * x1) + (-13 * x2) + (25 * x3) < -4 ; -ASSERT (-24 * x0) + (-22 * x1) + (-21 * x2) + (-6 * x3) > -21 ; -ASSERT (17 * x0) + (-21 * x1) + (25 * x2) + (-13 * x3) >= 16 ; -ASSERT (14 * x0) + (-25 * x1) + (-22 * x2) + (18 * x3) >= -30 ; -ASSERT (-27 * x0) + (8 * x1) + (-12 * x2) + (26 * x3) >= 15 ; -ASSERT (-31 * x0) + (2 * x1) + (19 * x2) + (-11 * x3) >= -27 ; -ASSERT (32 * x0) + (-29 * x1) + (9 * x2) + (-4 * x3) < 3 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-060.cvc b/test/regress/regress1/arith/arith-int-060.cvc deleted file mode 100644 index 74dd16dca..000000000 --- a/test/regress/regress1/arith/arith-int-060.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% 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 ; -ASSERT (-21 * x0) + (26 * x1) + (-10 * x2) + (-28 * x3) = 5; -ASSERT (2 * x0) + (-15 * x1) + (12 * x2) + (22 * x3) < -22 ; -ASSERT (10 * x0) + (24 * x1) + (11 * x2) + (-17 * x3) < 17 ; -ASSERT (26 * x0) + (32 * x1) + (-17 * x2) + (-3 * x3) >= 20 ; -ASSERT (11 * x0) + (26 * x1) + (-23 * x2) + (22 * x3) <= 32 ; -ASSERT (-19 * x0) + (22 * x1) + (-21 * x2) + (-28 * x3) <= -5 ; -ASSERT (-5 * x0) + (-18 * x1) + (10 * x2) + (-27 * x3) < -26 ; -ASSERT (21 * x0) + (-26 * x1) + (25 * x2) + (-13 * x3) < 15 ; -ASSERT (22 * x0) + (-2 * x1) + (3 * x2) + (-21 * x3) < 7 ; -ASSERT (20 * x0) + (-3 * x1) + (27 * x2) + (-21 * x3) < -18 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-061.cvc b/test/regress/regress1/arith/arith-int-061.cvc deleted file mode 100644 index b3bd247b2..000000000 --- a/test/regress/regress1/arith/arith-int-061.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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 ; -ASSERT (-25 * x0) + (19 * x1) + (-26 * x2) + (-20 * x3) = 22 ; -ASSERT (-11 * x0) + (28 * x1) + (-16 * x2) + (-15 * x3) = 15 ; -ASSERT (-11 * x0) + (-25 * x1) + (-16 * x2) + (25 * x3) = -3 ; -ASSERT (-15 * x0) + (-25 * x1) + (11 * x2) + (-24 * x3) = 29 ; -ASSERT (-12 * x0) + (-32 * x1) + (-28 * x2) + (-27 * x3) = -7 ; -ASSERT (16 * x0) + (5 * x1) + (10 * x2) + (-18 * x3) = 18 ; -ASSERT (-2 * x0) + (5 * x1) + (30 * x2) + (29 * x3) = -29 ; -ASSERT (-14 * x0) + (-20 * x1) + (21 * x2) + (1 * x3) = 31 ; -ASSERT (15 * x0) + (-7 * x1) + (-3 * x2) + (-24 * x3) > 3 ; -ASSERT (-16 * x0) + (-30 * x1) + (-31 * x2) + (16 * x3) > -9 ; -ASSERT (12 * x0) + (27 * x1) + (-11 * x2) + (-10 * x3) > -6 ; -ASSERT (0 * x0) + (29 * x1) + (32 * x2) + (9 * x3) <= -24 ; -ASSERT (11 * x0) + (-7 * x1) + (24 * x2) + (-30 * x3) >= 8 ; -ASSERT (1 * x0) + (25 * x1) + (29 * x2) + (15 * x3) <= -13 ; -ASSERT (-25 * x0) + (31 * x1) + (-32 * x2) + (-1 * x3) <= 9 ; -ASSERT (-22 * x0) + (-23 * x1) + (-4 * x2) + (-12 * x3) > 32 ; -ASSERT (22 * x0) + (-1 * x1) + (27 * x2) + (-22 * x3) > 20 ; -ASSERT (-20 * x0) + (-21 * x1) + (1 * x2) + (-32 * x3) >= 16; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-062.cvc b/test/regress/regress1/arith/arith-int-062.cvc deleted file mode 100644 index 0a185eb68..000000000 --- a/test/regress/regress1/arith/arith-int-062.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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 ; -ASSERT (1 * x0) + (-23 * x1) + (22 * x2) + (10 * x3) = -18 ; -ASSERT (-13 * x0) + (-17 * x1) + (-8 * x2) + (-16 * x3) = 16 ; -ASSERT (24 * x0) + (-4 * x1) + (-26 * x2) + (9 * x3) = -26 ; -ASSERT (24 * x0) + (23 * x1) + (17 * x2) + (-10 * x3) >= 5 ; -ASSERT (-12 * x0) + (-12 * x1) + (-13 * x2) + (-22 * x3) <= 9 ; -ASSERT (-7 * x0) + (17 * x1) + (-24 * x2) + (-8 * x3) <= -31 ; -ASSERT (-28 * x0) + (-10 * x1) + (3 * x2) + (-23 * x3) <= -19 ; -ASSERT (12 * x0) + (-16 * x1) + (27 * x2) + (-28 * x3) > -27 ; -ASSERT (-15 * x0) + (-24 * x1) + (12 * x2) + (21 * x3) < 21 ; -ASSERT (6 * x0) + (31 * x1) + (5 * x2) + (-5 * x3) >= 10 ; -ASSERT (-7 * x0) + (-20 * x1) + (-9 * x2) + (-32 * x3) >= 7 ; -ASSERT (3 * x0) + (24 * x1) + (-18 * x2) + (-9 * x3) < -30 ; -ASSERT (-14 * x0) + (22 * x1) + (22 * x2) + (-22 * x3) < -16 ; -ASSERT (1 * x0) + (4 * x1) + (10 * x2) + (28 * x3) > -31 ; -ASSERT (-14 * x0) + (-15 * x1) + (-8 * x2) + (2 * x3) >= 3 ; -ASSERT (13 * x0) + (-27 * x1) + (-14 * x2) + (28 * x3) < 28 ; -ASSERT (26 * x0) + (-12 * x1) + (-21 * x2) + (-16 * x3) < -26 ; -ASSERT (-6 * x0) + (-19 * x1) + (-8 * x2) + (18 * x3) >= 27; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-063.cvc b/test/regress/regress1/arith/arith-int-063.cvc deleted file mode 100644 index 13c4aae2e..000000000 --- a/test/regress/regress1/arith/arith-int-063.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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 ; -ASSERT (6 * x0) + (-10 * x1) + (4 * x2) + (23 * x3) = 10; -ASSERT (-8 * x0) + (12 * x1) + (-19 * x2) + (-17 * x3) >= 21 ; -ASSERT (-20 * x0) + (6 * x1) + (-12 * x2) + (-31 * x3) > -31 ; -ASSERT (32 * x0) + (-6 * x1) + (-14 * x2) + (-32 * x3) >= 13 ; -ASSERT (29 * x0) + (12 * x1) + (17 * x2) + (9 * x3) > 32 ; -ASSERT (1 * x0) + (21 * x1) + (12 * x2) + (23 * x3) <= 14 ; -ASSERT (-12 * x0) + (-9 * x1) + (26 * x2) + (26 * x3) < 3 ; -ASSERT (-8 * x0) + (27 * x1) + (29 * x2) + (-10 * x3) >= 22 ; -ASSERT (-15 * x0) + (29 * x1) + (29 * x2) + (17 * x3) <= 22 ; -ASSERT (-4 * x0) + (0 * x1) + (1 * x2) + (-24 * x3) < -24 ; -ASSERT (25 * x0) + (17 * x1) + (31 * x2) + (-28 * x3) >= -12 ; -ASSERT (32 * x0) + (8 * x1) + (-3 * x2) + (19 * x3) > -19 ; -ASSERT (-27 * x0) + (-18 * x1) + (18 * x2) + (22 * x3) > 26 ; -ASSERT (29 * x0) + (29 * x1) + (4 * x2) + (-6 * x3) >= 8 ; -ASSERT (-12 * x0) + (17 * x1) + (-22 * x2) + (1 * x3) < 30 ; -ASSERT (-24 * x0) + (16 * x1) + (-26 * x2) + (-27 * x3) > 29 ; -ASSERT (9 * x0) + (15 * x1) + (-28 * x2) + (0 * x3) > -2 ; -ASSERT (-5 * x0) + (30 * x1) + (-21 * x2) + (-6 * x3) >= 12 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-064.cvc b/test/regress/regress1/arith/arith-int-064.cvc deleted file mode 100644 index f50b3cd97..000000000 --- a/test/regress/regress1/arith/arith-int-064.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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 ; -ASSERT (-6 * x0) + (17 * x1) + (-20 * x2) + (11 * x3) < -5 ; -ASSERT (15 * x0) + (-15 * x1) + (-13 * x2) + (-21 * x3) < 27 ; -ASSERT (-24 * x0) + (-22 * x1) + (5 * x2) + (22 * x3) < 23 ; -ASSERT (27 * x0) + (23 * x1) + (-19 * x2) + (20 * x3) >= -8 ; -ASSERT (27 * x0) + (-27 * x1) + (23 * x2) + (17 * x3) < -5 ; -ASSERT (-11 * x0) + (-8 * x1) + (14 * x2) + (-10 * x3) <= 1 ; -ASSERT (12 * x0) + (7 * x1) + (-26 * x2) + (-28 * x3) >= -7 ; -ASSERT (25 * x0) + (-25 * x1) + (5 * x2) + (32 * x3) > -10 ; -ASSERT (-29 * x0) + (-24 * x1) + (26 * x2) + (-31 * x3) < -16 ; -ASSERT (10 * x0) + (29 * x1) + (9 * x2) + (23 * x3) < 13 ; -ASSERT (-26 * x0) + (6 * x1) + (-14 * x2) + (-21 * x3) > -15 ; -ASSERT (24 * x0) + (-14 * x1) + (-32 * x2) + (22 * x3) > -31 ; -ASSERT (-31 * x0) + (-16 * x1) + (-9 * x2) + (-32 * x3) > -19 ; -ASSERT (-1 * x0) + (17 * x1) + (26 * x2) + (-16 * x3) > -27 ; -ASSERT (10 * x0) + (-11 * x1) + (-20 * x2) + (-25 * x3) < -30 ; -ASSERT (-16 * x0) + (9 * x1) + (-10 * x2) + (-8 * x3) < -9 ; -ASSERT (19 * x0) + (10 * x1) + (18 * x2) + (7 * x3) < -30 ; -ASSERT (20 * x0) + (-25 * x1) + (-18 * x2) + (-2 * x3) <= -11; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-065.cvc b/test/regress/regress1/arith/arith-int-065.cvc deleted file mode 100644 index 354eb981c..000000000 --- a/test/regress/regress1/arith/arith-int-065.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% 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 ; -ASSERT (32 * x0) + (-2 * x1) + (14 * x2) + (5 * x3) = -15 ; -ASSERT (-16 * x0) + (22 * x1) + (0 * x2) + (-26 * x3) >= 18 ; -ASSERT (11 * x0) + (-19 * x1) + (10 * x2) + (26 * x3) >= -20 ; -ASSERT (-25 * x0) + (-24 * x1) + (12 * x2) + (4 * x3) >= -14 ; -ASSERT (-20 * x0) + (-10 * x1) + (21 * x2) + (23 * x3) >= 28 ; -ASSERT (6 * x0) + (-31 * x1) + (11 * x2) + (-3 * x3) <= 4 ; -ASSERT (2 * x0) + (11 * x1) + (-13 * x2) + (-16 * x3) >= 23 ; -ASSERT (-6 * x0) + (-24 * x1) + (24 * x2) + (7 * x3) <= 14 ; -ASSERT (0 * x0) + (3 * x1) + (-14 * x2) + (-19 * x3) >= 15 ; -ASSERT (-31 * x0) + (-27 * x1) + (-32 * x2) + (-28 * x3) <= -15 ; -ASSERT (-11 * x0) + (3 * x1) + (-6 * x2) + (-5 * x3) < -31 ; -ASSERT (-2 * x0) + (-21 * x1) + (2 * x2) + (28 * x3) >= 7 ; -ASSERT (-12 * x0) + (19 * x1) + (-17 * x2) + (-14 * x3) > 11 ; -ASSERT (32 * x0) + (-29 * x1) + (-12 * x2) + (24 * x3) < -9 ; -ASSERT (-19 * x0) + (1 * x1) + (8 * x2) + (4 * x3) <= 3 ; -ASSERT (13 * x0) + (17 * x1) + (22 * x2) + (13 * x3) <= -25 ; -ASSERT (2 * x0) + (-4 * x1) + (-3 * x2) + (19 * x3) <= -12 ; -ASSERT (-16 * x0) + (-20 * x1) + (21 * x2) + (-30 * x3) <= 2; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-066.cvc b/test/regress/regress1/arith/arith-int-066.cvc deleted file mode 100644 index f53a254bd..000000000 --- a/test/regress/regress1/arith/arith-int-066.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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 ; -ASSERT (-9 * x0) + (14 * x1) + (-16 * x2) + (15 * x3) > 18 ; -ASSERT (-28 * x0) + (-25 * x1) + (-10 * x2) + (-10 * x3) < -10 ; -ASSERT (19 * x0) + (-4 * x1) + (11 * x2) + (22 * x3) <= -6 ; -ASSERT (2 * x0) + (32 * x1) + (-16 * x2) + (-29 * x3) > 6 ; -ASSERT (-7 * x0) + (9 * x1) + (-25 * x2) + (6 * x3) <= 5 ; -ASSERT (4 * x0) + (-18 * x1) + (-21 * x2) + (12 * x3) >= -32 ; -ASSERT (-27 * x0) + (11 * x1) + (-3 * x2) + (-6 * x3) < 1 ; -ASSERT (10 * x0) + (13 * x1) + (11 * x2) + (28 * x3) > -15 ; -ASSERT (-1 * x0) + (-4 * x1) + (30 * x2) + (6 * x3) > 9 ; -ASSERT (19 * x0) + (14 * x1) + (17 * x2) + (-8 * x3) <= -21 ; -ASSERT (-15 * x0) + (20 * x1) + (9 * x2) + (19 * x3) <= 4 ; -ASSERT (-9 * x0) + (-22 * x1) + (29 * x2) + (-6 * x3) <= 3; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-067.cvc b/test/regress/regress1/arith/arith-int-067.cvc deleted file mode 100644 index 61159e9aa..000000000 --- a/test/regress/regress1/arith/arith-int-067.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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 ; -ASSERT (22 * x0) + (6 * x1) + (-9 * x2) + (27 * x3) = 10 ; -ASSERT (1 * x0) + (-26 * x1) + (27 * x2) + (-19 * x3) = 29 ; -ASSERT (-13 * x0) + (18 * x1) + (5 * x2) + (22 * x3) < -10 ; -ASSERT (5 * x0) + (1 * x1) + (4 * x2) + (-7 * x3) > -12 ; -ASSERT (-30 * x0) + (-12 * x1) + (-22 * x2) + (-32 * x3) <= 1 ; -ASSERT (-15 * x0) + (19 * x1) + (22 * x2) + (-9 * x3) >= 12 ; -ASSERT (-6 * x0) + (-16 * x1) + (30 * x2) + (-13 * x3) <= -9 ; -ASSERT (-3 * x0) + (1 * x1) + (10 * x2) + (7 * x3) < -32 ; -ASSERT (5 * x0) + (-17 * x1) + (25 * x2) + (-31 * x3) >= -6 ; -ASSERT (18 * x0) + (28 * x1) + (-6 * x2) + (10 * x3) <= -31 ; -ASSERT (-11 * x0) + (-25 * x1) + (2 * x2) + (-3 * x3) > -3 ; -ASSERT (-14 * x0) + (-28 * x1) + (-2 * x2) + (20 * x3) < -25; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-068.cvc b/test/regress/regress1/arith/arith-int-068.cvc deleted file mode 100644 index 683d36801..000000000 --- a/test/regress/regress1/arith/arith-int-068.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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 ; -ASSERT (31 * x0) + (-32 * x1) + (27 * x2) + (29 * x3) = 23 ; -ASSERT (8 * x0) + (-19 * x1) + (-7 * x2) + (0 * x3) <= -1 ; -ASSERT (-32 * x0) + (30 * x1) + (9 * x2) + (-21 * x3) <= 24 ; -ASSERT (15 * x0) + (-4 * x1) + (27 * x2) + (-26 * x3) >= 23 ; -ASSERT (7 * x0) + (26 * x1) + (-16 * x2) + (21 * x3) >= 16 ; -ASSERT (-24 * x0) + (-17 * x1) + (-9 * x2) + (27 * x3) <= 2 ; -ASSERT (29 * x0) + (-7 * x1) + (-8 * x2) + (32 * x3) <= -2 ; -ASSERT (32 * x0) + (31 * x1) + (7 * x2) + (-26 * x3) < 1 ; -ASSERT (-17 * x0) + (-13 * x1) + (-20 * x2) + (29 * x3) >= -21 ; -ASSERT (-32 * x0) + (27 * x1) + (-29 * x2) + (-11 * x3) >= -23 ; -ASSERT (29 * x0) + (-4 * x1) + (21 * x2) + (-16 * x3) < 23 ; -ASSERT (-15 * x0) + (26 * x1) + (14 * x2) + (13 * x3) <= -29; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-069.cvc b/test/regress/regress1/arith/arith-int-069.cvc deleted file mode 100644 index 356a28013..000000000 --- a/test/regress/regress1/arith/arith-int-069.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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 ; -ASSERT (13 * x0) + (27 * x1) + (-17 * x2) + (25 * x3) <= -17 ; -ASSERT (27 * x0) + (-30 * x1) + (-16 * x2) + (-3 * x3) > -19 ; -ASSERT (-18 * x0) + (-25 * x1) + (-5 * x2) + (3 * x3) < -10 ; -ASSERT (9 * x0) + (-32 * x1) + (30 * x2) + (11 * x3) >= 23 ; -ASSERT (14 * x0) + (18 * x1) + (-21 * x2) + (-19 * x3) > 9 ; -ASSERT (28 * x0) + (2 * x1) + (23 * x2) + (17 * x3) < -6 ; -ASSERT (13 * x0) + (-17 * x1) + (-1 * x2) + (29 * x3) < -22 ; -ASSERT (-19 * x0) + (22 * x1) + (6 * x2) + (12 * x3) <= -9 ; -ASSERT (24 * x0) + (-14 * x1) + (31 * x2) + (12 * x3) > -26 ; -ASSERT (-1 * x0) + (24 * x1) + (-1 * x2) + (-31 * x3) > -21 ; -ASSERT (-22 * x0) + (28 * x1) + (-27 * x2) + (0 * x3) >= 3 ; -ASSERT (-28 * x0) + (29 * x1) + (-3 * x2) + (-22 * x3) >= -23; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-070.cvc b/test/regress/regress1/arith/arith-int-070.cvc deleted file mode 100644 index 791b3b8af..000000000 --- a/test/regress/regress1/arith/arith-int-070.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% 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 ; -ASSERT (-3 * x0) + (-28 * x1) + (-15 * x2) + (7 * x3) = -9 ; -ASSERT (27 * x0) + (4 * x1) + (-31 * x2) + (-32 * x3) <= -12 ; -ASSERT (16 * x0) + (6 * x1) + (17 * x2) + (22 * x3) <= 5 ; -ASSERT (-27 * x0) + (-16 * x1) + (1 * x2) + (23 * x3) >= 9 ; -ASSERT (21 * x0) + (-28 * x1) + (-26 * x2) + (-26 * x3) <= -25 ; -ASSERT (-12 * x0) + (-32 * x1) + (-22 * x2) + (-20 * x3) > -32 ; -ASSERT (26 * x0) + (26 * x1) + (30 * x2) + (4 * x3) < 21 ; -ASSERT (-22 * x0) + (-21 * x1) + (0 * x2) + (30 * x3) < 13 ; -ASSERT (13 * x0) + (17 * x1) + (-7 * x2) + (-31 * x3) < 29 ; -ASSERT (-12 * x0) + (30 * x1) + (1 * x2) + (4 * x3) > -24 ; -ASSERT (-23 * x0) + (-2 * x1) + (29 * x2) + (11 * x3) > 26 ; -ASSERT (-18 * x0) + (-16 * x1) + (31 * x2) + (14 * x3) <= 32; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-071.cvc b/test/regress/regress1/arith/arith-int-071.cvc deleted file mode 100644 index d44b18b45..000000000 --- a/test/regress/regress1/arith/arith-int-071.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 ; -ASSERT (-5 * x0) + (16 * x1) + (-15 * x2) + (-13 * x3) > 27 ; -ASSERT (16 * x0) + (-4 * x1) + (17 * x2) + (-24 * x3) > -9 ; -ASSERT (3 * x0) + (13 * x1) + (-15 * x2) + (-13 * x3) <= -32 ; -ASSERT (-18 * x0) + (21 * x1) + (-7 * x2) + (2 * x3) >= 13 ; -ASSERT (5 * x0) + (11 * x1) + (-11 * x2) + (-11 * x3) <= 9 ; -ASSERT (-9 * x0) + (8 * x1) + (-25 * x2) + (-14 * x3) >= 10 ; -ASSERT (17 * x0) + (-29 * x1) + (23 * x2) + (7 * x3) <= -31 ; -ASSERT (20 * x0) + (0 * x1) + (1 * x2) + (-6 * x3) <= 23 ; -ASSERT (-25 * x0) + (0 * x1) + (-32 * x2) + (17 * x3) > -14 ; -ASSERT (6 * x0) + (-30 * x1) + (-11 * x2) + (29 * x3) < 28 ; -ASSERT (-19 * x0) + (23 * x1) + (-19 * x2) + (3 * x3) >= 7 ; -ASSERT (29 * x0) + (21 * x1) + (-28 * x2) + (-28 * x3) < 22 ; -ASSERT (28 * x0) + (25 * x1) + (2 * x2) + (-23 * x3) <= -28; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-072.cvc b/test/regress/regress1/arith/arith-int-072.cvc deleted file mode 100644 index fb13a6616..000000000 --- a/test/regress/regress1/arith/arith-int-072.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 ; -ASSERT (-31 * x0) + (28 * x1) + (-4 * x2) + (31 * x3) = -32 ; -ASSERT (1 * x0) + (-12 * x1) + (29 * x2) + (-6 * x3) = 25 ; -ASSERT (2 * x0) + (7 * x1) + (-24 * x2) + (28 * x3) >= -12 ; -ASSERT (-23 * x0) + (-22 * x1) + (14 * x2) + (-24 * x3) >= 22 ; -ASSERT (23 * x0) + (-21 * x1) + (22 * x2) + (26 * x3) >= -4 ; -ASSERT (25 * x0) + (27 * x1) + (14 * x2) + (5 * x3) <= 9 ; -ASSERT (16 * x0) + (2 * x1) + (24 * x2) + (-11 * x3) < -32 ; -ASSERT (0 * x0) + (23 * x1) + (29 * x2) + (-15 * x3) < -14 ; -ASSERT (5 * x0) + (-12 * x1) + (-7 * x2) + (29 * x3) <= -16 ; -ASSERT (25 * x0) + (26 * x1) + (14 * x2) + (-2 * x3) <= 13 ; -ASSERT (-30 * x0) + (19 * x1) + (24 * x2) + (7 * x3) < -23 ; -ASSERT (24 * x0) + (28 * x1) + (12 * x2) + (-25 * x3) >= -22 ; -ASSERT (27 * x0) + (-13 * x1) + (-16 * x2) + (-3 * x3) < 24; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-073.cvc b/test/regress/regress1/arith/arith-int-073.cvc deleted file mode 100644 index 784190cad..000000000 --- a/test/regress/regress1/arith/arith-int-073.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 ; -ASSERT (-4 * x0) + (16 * x1) + (3 * x2) + (-1 * x3) = 12 ; -ASSERT (2 * x0) + (24 * x1) + (-7 * x2) + (4 * x3) = 24 ; -ASSERT (26 * x0) + (-8 * x1) + (28 * x2) + (9 * x3) = -12 ; -ASSERT (19 * x0) + (-3 * x1) + (25 * x2) + (10 * x3) <= -19 ; -ASSERT (-13 * x0) + (-16 * x1) + (-14 * x2) + (8 * x3) <= 25 ; -ASSERT (-21 * x0) + (-2 * x1) + (-20 * x2) + (8 * x3) <= -22 ; -ASSERT (16 * x0) + (4 * x1) + (11 * x2) + (-15 * x3) >= -12 ; -ASSERT (-24 * x0) + (-8 * x1) + (2 * x2) + (-24 * x3) <= -22 ; -ASSERT (29 * x0) + (23 * x1) + (-20 * x2) + (8 * x3) > 21 ; -ASSERT (-24 * x0) + (-28 * x1) + (-23 * x2) + (-24 * x3) < -5 ; -ASSERT (-1 * x0) + (17 * x1) + (19 * x2) + (-7 * x3) > -5 ; -ASSERT (24 * x0) + (3 * x1) + (6 * x2) + (10 * x3) <= 15 ; -ASSERT (27 * x0) + (-11 * x1) + (-8 * x2) + (-22 * x3) > -30; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-074.cvc b/test/regress/regress1/arith/arith-int-074.cvc deleted file mode 100644 index 914cbe8e3..000000000 --- a/test/regress/regress1/arith/arith-int-074.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 ; -ASSERT (24 * x0) + (-10 * x1) + (19 * x2) + (7 * x3) = -30 ; -ASSERT (1 * x0) + (-12 * x1) + (-13 * x2) + (-17 * x3) = -28 ; -ASSERT (-17 * x0) + (14 * x1) + (7 * x2) + (-18 * x3) = -14 ; -ASSERT (7 * x0) + (14 * x1) + (-22 * x2) + (29 * x3) = -6; -ASSERT (15 * x0) + (-6 * x1) + (3 * x2) + (-19 * x3) > 26 ; -ASSERT (-20 * x0) + (-18 * x1) + (-24 * x2) + (5 * x3) >= -1 ; -ASSERT (11 * x0) + (-26 * x1) + (-20 * x2) + (-16 * x3) > -7 ; -ASSERT (31 * x0) + (-2 * x1) + (6 * x2) + (32 * x3) > -22 ; -ASSERT (-25 * x0) + (26 * x1) + (-26 * x2) + (-21 * x3) >= -27 ; -ASSERT (-17 * x0) + (-30 * x1) + (14 * x2) + (17 * x3) <= -19 ; -ASSERT (-16 * x0) + (4 * x1) + (1 * x2) + (-24 * x3) <= -24 ; -ASSERT (-13 * x0) + (29 * x1) + (-27 * x2) + (12 * x3) < -15 ; -ASSERT (26 * x0) + (-2 * x1) + (-28 * x2) + (20 * x3) < -20 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-075.cvc b/test/regress/regress1/arith/arith-int-075.cvc deleted file mode 100644 index d3851e284..000000000 --- a/test/regress/regress1/arith/arith-int-075.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% 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 ; -ASSERT (11 * x0) + (9 * x1) + (32 * x2) + (-15 * x3) > 21 ; -ASSERT (12 * x0) + (1 * x1) + (25 * x2) + (-17 * x3) > -13 ; -ASSERT (-20 * x0) + (7 * x1) + (13 * x2) + (-15 * x3) <= -3 ; -ASSERT (32 * x0) + (4 * x1) + (-30 * x2) + (13 * x3) <= -15 ; -ASSERT (-32 * x0) + (-27 * x1) + (20 * x2) + (22 * x3) <= -28 ; -ASSERT (28 * x0) + (23 * x1) + (10 * x2) + (20 * x3) < 9 ; -ASSERT (-30 * x0) + (-32 * x1) + (-28 * x2) + (-30 * x3) > 17 ; -ASSERT (-26 * x0) + (14 * x1) + (30 * x2) + (31 * x3) < 20 ; -ASSERT (21 * x0) + (23 * x1) + (-7 * x2) + (-16 * x3) > -19 ; -ASSERT (6 * x0) + (0 * x1) + (0 * x2) + (21 * x3) < -1 ; -ASSERT (13 * x0) + (29 * x1) + (17 * x2) + (-29 * x3) < -32 ; -ASSERT (22 * x0) + (-9 * x1) + (-25 * x2) + (11 * x3) > 29 ; -ASSERT (-25 * x0) + (-19 * x1) + (22 * x2) + (-27 * x3) >= 10; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-076.cvc b/test/regress/regress1/arith/arith-int-076.cvc deleted file mode 100644 index 25a3a7d35..000000000 --- a/test/regress/regress1/arith/arith-int-076.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% 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 ; -ASSERT (-23 * x0) + (-8 * x1) + (-12 * x2) + (-14 * x3) >= -25 ; -ASSERT (13 * x0) + (30 * x1) + (-12 * x2) + (22 * x3) < -12 ; -ASSERT (-12 * x0) + (-17 * x1) + (20 * x2) + (14 * x3) > -26 ; -ASSERT (-13 * x0) + (-17 * x1) + (-25 * x2) + (27 * x3) <= -29 ; -ASSERT (-8 * x0) + (-31 * x1) + (-3 * x2) + (-22 * x3) > -22 ; -ASSERT (30 * x0) + (11 * x1) + (-32 * x2) + (32 * x3) >= 28; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-077.cvc b/test/regress/regress1/arith/arith-int-077.cvc deleted file mode 100644 index 7e4482093..000000000 --- a/test/regress/regress1/arith/arith-int-077.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% 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; -ASSERT (3 * x0) + (17 * x1) + (30 * x2) + (31 * x3) < 13 ; -ASSERT (-17 * x0) + (-21 * x1) + (10 * x2) + (8 * x3) > 23 ; -ASSERT (-14 * x0) + (10 * x1) + (11 * x2) + (27 * x3) > -13 ; -ASSERT (-14 * x0) + (24 * x1) + (3 * x2) + (-26 * x3) > 1 ; -ASSERT (-14 * x0) + (20 * x1) + (-2 * x2) + (-24 * x3) > -26 ; -ASSERT (20 * x0) + (-23 * x1) + (30 * x2) + (-30 * x3) < 24 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-078.cvc b/test/regress/regress1/arith/arith-int-078.cvc deleted file mode 100644 index eacccc375..000000000 --- a/test/regress/regress1/arith/arith-int-078.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% 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 ; -ASSERT (-28 * x0) + (20 * x1) + (-9 * x2) + (9 * x3) = -3 ; -ASSERT (24 * x0) + (22 * x1) + (24 * x2) + (20 * x3) = 5; -ASSERT (-1 * x0) + (-12 * x1) + (20 * x2) + (26 * x3) >= 22 ; -ASSERT (-23 * x0) + (-20 * x1) + (-8 * x2) + (1 * x3) < 2 ; -ASSERT (5 * x0) + (-27 * x1) + (-24 * x2) + (25 * x3) > -21 ; -ASSERT (1 * x0) + (-8 * x1) + (-17 * x2) + (-27 * x3) < -24 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-080.cvc b/test/regress/regress1/arith/arith-int-080.cvc deleted file mode 100644 index bf6b90c67..000000000 --- a/test/regress/regress1/arith/arith-int-080.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% 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; -ASSERT (9 * x0) + (-26 * x1) + (-16 * x2) + (-9 * x3) >= 28 ; -ASSERT (14 * x0) + (-32 * x1) + (-31 * x2) + (0 * x3) >= 30 ; -ASSERT (-31 * x0) + (-27 * x1) + (23 * x2) + (4 * x3) >= 21 ; -ASSERT (27 * x0) + (-30 * x1) + (8 * x2) + (13 * x3) < 31 ; -ASSERT (-1 * x0) + (-29 * x1) + (23 * x2) + (10 * x3) < -10 ; -ASSERT (15 * x0) + (-2 * x1) + (22 * x2) + (-28 * x3) >= 2 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-081.cvc b/test/regress/regress1/arith/arith-int-081.cvc deleted file mode 100644 index 47cc66ae2..000000000 --- a/test/regress/regress1/arith/arith-int-081.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% 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 ; -ASSERT (-6 * x0) + (17 * x1) + (27 * x2) + (26 * x3) >= -30 ; -ASSERT (-19 * x0) + (-15 * x1) + (5 * x2) + (-27 * x3) < -3 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-082.cvc b/test/regress/regress1/arith/arith-int-082.cvc deleted file mode 100644 index a6245f036..000000000 --- a/test/regress/regress1/arith/arith-int-082.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% 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 ; -ASSERT (30 * x0) + (17 * x1) + (-3 * x2) + (-31 * x3) > 10 ; -ASSERT (2 * x0) + (9 * x1) + (9 * x2) + (-16 * x3) <= 11; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-083.cvc b/test/regress/regress1/arith/arith-int-083.cvc deleted file mode 100644 index 3a7c635cc..000000000 --- a/test/regress/regress1/arith/arith-int-083.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% 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 ; -ASSERT (7 * x0) + (17 * x1) + (-20 * x2) + (13 * x3) > -26 ; -ASSERT (-17 * x0) + (14 * x1) + (-23 * x2) + (17 * x3) <= -27; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-086.cvc b/test/regress/regress1/arith/arith-int-086.cvc deleted file mode 100644 index 6ee96589b..000000000 --- a/test/regress/regress1/arith/arith-int-086.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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 ; -ASSERT (19 * x0) + (28 * x1) + (-15 * x2) + (18 * x3) < -9 ; -ASSERT (-10 * x0) + (1 * x1) + (-3 * x2) + (6 * x3) <= 1 ; -ASSERT (-15 * x0) + (-32 * x1) + (28 * x2) + (6 * x3) >= -8 ; -ASSERT (-18 * x0) + (-16 * x1) + (15 * x2) + (-28 * x3) <= 1 ; -ASSERT (-20 * x0) + (-31 * x1) + (20 * x2) + (13 * x3) >= -7 ; -ASSERT (29 * x0) + (16 * x1) + (7 * x2) + (14 * x3) < 11 ; -ASSERT (-10 * x0) + (22 * x1) + (25 * x2) + (24 * x3) >= 5 ; -ASSERT (-3 * x0) + (11 * x1) + (27 * x2) + (11 * x3) <= 9; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-087.cvc b/test/regress/regress1/arith/arith-int-087.cvc deleted file mode 100644 index b969df1a3..000000000 --- a/test/regress/regress1/arith/arith-int-087.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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 ; -ASSERT (-19 * x0) + (-27 * x1) + (-31 * x2) + (15 * x3) = 12; -ASSERT (10 * x0) + (-10 * x1) + (25 * x2) + (-3 * x3) < -30 ; -ASSERT (5 * x0) + (-18 * x1) + (21 * x2) + (-28 * x3) <= -4 ; -ASSERT (-6 * x0) + (15 * x1) + (-10 * x2) + (0 * x3) < -20 ; -ASSERT (10 * x0) + (23 * x1) + (-20 * x2) + (12 * x3) >= -15 ; -ASSERT (-31 * x0) + (-30 * x1) + (12 * x2) + (11 * x3) > 29 ; -ASSERT (26 * x0) + (23 * x1) + (28 * x2) + (-5 * x3) > 8 ; -ASSERT (6 * x0) + (-29 * x1) + (12 * x2) + (16 * x3) < 27 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-088.cvc b/test/regress/regress1/arith/arith-int-088.cvc deleted file mode 100644 index de0d23844..000000000 --- a/test/regress/regress1/arith/arith-int-088.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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 ; -ASSERT (7 * x0) + (28 * x1) + (6 * x2) + (-20 * x3) <= -16 ; -ASSERT (-15 * x0) + (21 * x1) + (5 * x2) + (-2 * x3) <= 11 ; -ASSERT (-5 * x0) + (-16 * x1) + (-16 * x2) + (14 * x3) <= 12 ; -ASSERT (3 * x0) + (28 * x1) + (22 * x2) + (-6 * x3) >= -31 ; -ASSERT (15 * x0) + (-13 * x1) + (10 * x2) + (21 * x3) <= -25 ; -ASSERT (1 * x0) + (-24 * x1) + (-30 * x2) + (25 * x3) > 17 ; -ASSERT (12 * x0) + (-3 * x1) + (0 * x2) + (23 * x3) < -12 ; -ASSERT (16 * x0) + (-9 * x1) + (1 * x2) + (-15 * x3) < -6; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-089.cvc b/test/regress/regress1/arith/arith-int-089.cvc deleted file mode 100644 index e50daa9de..000000000 --- a/test/regress/regress1/arith/arith-int-089.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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 ; -ASSERT (19 * x0) + (-7 * x1) + (-15 * x2) + (12 * x3) = 32 ; -ASSERT (5 * x0) + (32 * x1) + (22 * x2) + (1 * x3) = -13 ; -ASSERT (-12 * x0) + (-9 * x1) + (-30 * x2) + (-13 * x3) >= 0 ; -ASSERT (-9 * x0) + (7 * x1) + (-24 * x2) + (22 * x3) >= 11 ; -ASSERT (28 * x0) + (-5 * x1) + (12 * x2) + (15 * x3) >= 31 ; -ASSERT (5 * x0) + (-6 * x1) + (5 * x2) + (-2 * x3) >= -5 ; -ASSERT (-14 * x0) + (-17 * x1) + (-29 * x2) + (-8 * x3) < -32 ; -ASSERT (20 * x0) + (-19 * x1) + (-27 * x2) + (-20 * x3) >= -2; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-090.cvc b/test/regress/regress1/arith/arith-int-090.cvc deleted file mode 100644 index 74d4ba4db..000000000 --- a/test/regress/regress1/arith/arith-int-090.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% 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 ; -ASSERT (10 * x0) + (19 * x1) + (-10 * x2) + (-2 * x3) > -31 ; -ASSERT (-31 * x0) + (17 * x1) + (15 * x2) + (31 * x3) > -12 ; -ASSERT (-17 * x0) + (16 * x1) + (17 * x2) + (-11 * x3) >= 17 ; -ASSERT (19 * x0) + (-31 * x1) + (-16 * x2) + (-29 * x3) >= 15 ; -ASSERT (24 * x0) + (-32 * x1) + (27 * x2) + (11 * x3) < 26 ; -ASSERT (-2 * x0) + (5 * x1) + (-21 * x2) + (24 * x3) >= -17 ; -ASSERT (13 * x0) + (11 * x1) + (-28 * x2) + (-5 * x3) > 16 ; -ASSERT (-16 * x0) + (17 * x1) + (22 * x2) + (6 * x3) > 21; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-091.cvc b/test/regress/regress1/arith/arith-int-091.cvc deleted file mode 100644 index c03b544a3..000000000 --- a/test/regress/regress1/arith/arith-int-091.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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 ; -ASSERT (15 * x0) + (9 * x1) + (-13 * x2) + (-21 * x3) = -13 ; -ASSERT (-4 * x0) + (16 * x1) + (-5 * x2) + (8 * x3) = -25 ; -ASSERT (-11 * x0) + (26 * x1) + (1 * x2) + (23 * x3) < 6 ; -ASSERT (-31 * x0) + (-25 * x1) + (1 * x2) + (16 * x3) > -8 ; -ASSERT (9 * x0) + (-19 * x1) + (28 * x2) + (15 * x3) < -30 ; -ASSERT (32 * x0) + (18 * x1) + (2 * x2) + (31 * x3) > -7 ; -ASSERT (24 * x0) + (29 * x1) + (20 * x2) + (-16 * x3) >= 3 ; -ASSERT (-1 * x0) + (17 * x1) + (-27 * x2) + (-32 * x3) >= 20 ; -ASSERT (26 * x0) + (-23 * x1) + (6 * x2) + (30 * x3) <= 5 ; -ASSERT (13 * x0) + (6 * x1) + (-26 * x2) + (1 * x3) > -29 ; -ASSERT (26 * x0) + (2 * x1) + (8 * x2) + (-18 * x3) <= 32 ; -ASSERT (-21 * x0) + (28 * x1) + (23 * x2) + (4 * x3) <= -31 ; -ASSERT (26 * x0) + (2 * x1) + (-28 * x2) + (12 * x3) > 6 ; -ASSERT (-20 * x0) + (-22 * x1) + (-16 * x2) + (-21 * x3) <= -1 ; -ASSERT (21 * x0) + (-22 * x1) + (19 * x2) + (32 * x3) <= -10 ; -ASSERT (3 * x0) + (28 * x1) + (-11 * x2) + (0 * x3) > 0 ; -ASSERT (-13 * x0) + (-16 * x1) + (-17 * x2) + (-2 * x3) <= -17; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-092.cvc b/test/regress/regress1/arith/arith-int-092.cvc deleted file mode 100644 index d080cde0c..000000000 --- a/test/regress/regress1/arith/arith-int-092.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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 ; -ASSERT (17 * x0) + (11 * x1) + (24 * x2) + (16 * x3) = -3 ; -ASSERT (15 * x0) + (-10 * x1) + (-15 * x2) + (25 * x3) = -30 ; -ASSERT (7 * x0) + (26 * x1) + (-8 * x2) + (-29 * x3) >= -32 ; -ASSERT (20 * x0) + (25 * x1) + (-23 * x2) + (13 * x3) >= -30 ; -ASSERT (27 * x0) + (-32 * x1) + (-27 * x2) + (13 * x3) >= -12 ; -ASSERT (25 * x0) + (-16 * x1) + (32 * x2) + (-6 * x3) >= -30 ; -ASSERT (32 * x0) + (-18 * x1) + (-6 * x2) + (-32 * x3) <= -26 ; -ASSERT (25 * x0) + (12 * x1) + (25 * x2) + (-14 * x3) > 5 ; -ASSERT (-4 * x0) + (-20 * x1) + (12 * x2) + (-30 * x3) >= 13 ; -ASSERT (8 * x0) + (18 * x1) + (0 * x2) + (-28 * x3) <= 18 ; -ASSERT (-32 * x0) + (-25 * x1) + (23 * x2) + (5 * x3) < 29 ; -ASSERT (7 * x0) + (19 * x1) + (2 * x2) + (-31 * x3) > 7 ; -ASSERT (24 * x0) + (-17 * x1) + (-31 * x2) + (31 * x3) > 0 ; -ASSERT (13 * x0) + (20 * x1) + (-1 * x2) + (17 * x3) > 1 ; -ASSERT (17 * x0) + (26 * x1) + (6 * x2) + (29 * x3) >= -10 ; -ASSERT (-25 * x0) + (4 * x1) + (-22 * x2) + (14 * x3) < -23 ; -ASSERT (24 * x0) + (2 * x1) + (4 * x2) + (2 * x3) < 1; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-093.cvc b/test/regress/regress1/arith/arith-int-093.cvc deleted file mode 100644 index e910def47..000000000 --- a/test/regress/regress1/arith/arith-int-093.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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 ; -ASSERT (-11 * x0) + (4 * x1) + (24 * x2) + (-6 * x3) <= -23 ; -ASSERT (3 * x0) + (5 * x1) + (-5 * x2) + (17 * x3) < -17 ; -ASSERT (-10 * x0) + (-20 * x1) + (-16 * x2) + (-29 * x3) >= 6 ; -ASSERT (-28 * x0) + (1 * x1) + (-22 * x2) + (-16 * x3) >= 4 ; -ASSERT (19 * x0) + (8 * x1) + (-8 * x2) + (-2 * x3) > -23 ; -ASSERT (11 * x0) + (17 * x1) + (30 * x2) + (31 * x3) < -32 ; -ASSERT (23 * x0) + (30 * x1) + (-12 * x2) + (16 * x3) <= 4 ; -ASSERT (-23 * x0) + (-8 * x1) + (21 * x2) + (21 * x3) <= -14 ; -ASSERT (13 * x0) + (15 * x1) + (-6 * x2) + (-1 * x3) >= -8 ; -ASSERT (-21 * x0) + (18 * x1) + (27 * x2) + (-16 * x3) <= 11 ; -ASSERT (30 * x0) + (-6 * x1) + (5 * x2) + (-27 * x3) <= -7 ; -ASSERT (0 * x0) + (3 * x1) + (13 * x2) + (28 * x3) > -21 ; -ASSERT (-15 * x0) + (-20 * x1) + (10 * x2) + (-23 * x3) < 27 ; -ASSERT (24 * x0) + (6 * x1) + (-29 * x2) + (1 * x3) <= -23 ; -ASSERT (-24 * x0) + (-14 * x1) + (-15 * x2) + (8 * x3) > -19 ; -ASSERT (17 * x0) + (15 * x1) + (8 * x2) + (-31 * x3) >= -16 ; -ASSERT (-19 * x0) + (7 * x1) + (-28 * x2) + (20 * x3) < -19; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-094.cvc b/test/regress/regress1/arith/arith-int-094.cvc deleted file mode 100644 index 2204bba4e..000000000 --- a/test/regress/regress1/arith/arith-int-094.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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 ; -ASSERT (5 * x0) + (14 * x1) + (7 * x2) + (-29 * x3) = 31 ; -ASSERT (17 * x0) + (8 * x1) + (23 * x2) + (-26 * x3) <= -12 ; -ASSERT (7 * x0) + (29 * x1) + (24 * x2) + (4 * x3) <= -21 ; -ASSERT (-16 * x0) + (7 * x1) + (7 * x2) + (-29 * x3) < -16 ; -ASSERT (-7 * x0) + (-11 * x1) + (-17 * x2) + (22 * x3) > -11 ; -ASSERT (-10 * x0) + (-17 * x1) + (21 * x2) + (29 * x3) > -7 ; -ASSERT (-28 * x0) + (-26 * x1) + (-24 * x2) + (-21 * x3) < -20 ; -ASSERT (-32 * x0) + (26 * x1) + (-8 * x2) + (2 * x3) >= -18 ; -ASSERT (18 * x0) + (-23 * x1) + (-26 * x2) + (-24 * x3) > -30 ; -ASSERT (-9 * x0) + (31 * x1) + (-26 * x2) + (-22 * x3) < -15 ; -ASSERT (27 * x0) + (-1 * x1) + (10 * x2) + (28 * x3) < -20 ; -ASSERT (-4 * x0) + (-22 * x1) + (-24 * x2) + (2 * x3) < -13 ; -ASSERT (-4 * x0) + (-23 * x1) + (-16 * x2) + (18 * x3) > -20 ; -ASSERT (13 * x0) + (-30 * x1) + (-3 * x2) + (-25 * x3) <= 31 ; -ASSERT (21 * x0) + (-28 * x1) + (22 * x2) + (19 * x3) > 7 ; -ASSERT (-2 * x0) + (-31 * x1) + (24 * x2) + (18 * x3) > 27 ; -ASSERT (-14 * x0) + (-5 * x1) + (-22 * x2) + (1 * x3) <= -15; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-095.cvc b/test/regress/regress1/arith/arith-int-095.cvc deleted file mode 100644 index e803dbe9b..000000000 --- a/test/regress/regress1/arith/arith-int-095.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% 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 ; -ASSERT (32 * x0) + (29 * x1) + (-1 * x2) + (-10 * x3) < -23 ; -ASSERT (6 * x0) + (-27 * x1) + (29 * x2) + (28 * x3) < 5 ; -ASSERT (-7 * x0) + (-7 * x1) + (-28 * x2) + (32 * x3) <= -32 ; -ASSERT (-10 * x0) + (20 * x1) + (-28 * x2) + (-28 * x3) >= -6 ; -ASSERT (-13 * x0) + (-9 * x1) + (4 * x2) + (-32 * x3) > -1 ; -ASSERT (-21 * x0) + (4 * x1) + (0 * x2) + (-13 * x3) >= -1 ; -ASSERT (18 * x0) + (-21 * x1) + (-16 * x2) + (24 * x3) <= -12 ; -ASSERT (18 * x0) + (-10 * x1) + (-10 * x2) + (-3 * x3) <= -10 ; -ASSERT (-32 * x0) + (9 * x1) + (-24 * x2) + (-19 * x3) < -4 ; -ASSERT (12 * x0) + (20 * x1) + (31 * x2) + (-25 * x3) <= 23 ; -ASSERT (-22 * x0) + (15 * x1) + (-12 * x2) + (-6 * x3) < 18 ; -ASSERT (-25 * x0) + (-8 * x1) + (32 * x2) + (26 * x3) > -20 ; -ASSERT (-30 * x0) + (27 * x1) + (0 * x2) + (27 * x3) >= 7 ; -ASSERT (-8 * x0) + (-2 * x1) + (-6 * x2) + (-21 * x3) <= 21 ; -ASSERT (8 * x0) + (-31 * x1) + (-4 * x2) + (1 * x3) > -11 ; -ASSERT (22 * x0) + (-25 * x1) + (-26 * x2) + (10 * x3) < -32 ; -ASSERT (-12 * x0) + (-13 * x1) + (15 * x2) + (4 * x3) < 26; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-096.cvc b/test/regress/regress1/arith/arith-int-096.cvc deleted file mode 100644 index 354ae180d..000000000 --- a/test/regress/regress1/arith/arith-int-096.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% 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; -ASSERT (-6 * x0) + (-5 * x1) + (-2 * x2) + (-9 * x3) > -3 ; -ASSERT (30 * x0) + (22 * x1) + (-20 * x2) + (1 * x3) > -12 ; -ASSERT (-8 * x0) + (-25 * x1) + (28 * x2) + (-25 * x3) <= -8 ; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-099.cvc b/test/regress/regress1/arith/arith-int-099.cvc deleted file mode 100644 index 57a45de03..000000000 --- a/test/regress/regress1/arith/arith-int-099.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% 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 ; -ASSERT (-10 * x0) + (16 * x1) + (31 * x2) + (19 * x3) >= -21 ; -ASSERT (-15 * x0) + (18 * x1) + (-16 * x2) + (7 * x3) <= -12 ; -ASSERT (14 * x0) + (-1 * x1) + (12 * x2) + (27 * x3) >= -12; -QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-100.cvc b/test/regress/regress1/arith/arith-int-100.cvc deleted file mode 100644 index 66be1f8f7..000000000 --- a/test/regress/regress1/arith/arith-int-100.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% 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 ; -ASSERT (25 * x0) + (25 * x1) + (-15 * x2) + (-32 * x3) > -31 ; -ASSERT (17 * x0) + (-26 * x1) + (9 * x2) + (-28 * x3) >= -29 ; -ASSERT (-10 * x0) + (-18 * x1) + (15 * x2) + (0 * x3) <= 32; -QUERY FALSE; |