diff options
Diffstat (limited to 'test/regress/regress0/arith/integers')
94 files changed, 2 insertions, 1409 deletions
diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index aa24e9c35..203598490 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -23,112 +23,16 @@ MAKEFLAGS = -k TESTS = \ - arith-int-004.cvc \ - arith-int-011.cvc \ - arith-int-012.cvc \ - arith-int-013.cvc \ - arith-int-022.cvc \ - arith-int-024.cvc \ arith-int-042.cvc \ - arith-int-042.min.cvc \ - arith-int-047.cvc \ - arith-int-048.cvc \ - arith-int-050.cvc \ - arith-int-084.cvc \ - arith-int-085.cvc \ - arith-int-097.cvc + arith-int-042.min.cvc EXTRA_DIST = $(TESTS) \ - arith-int-001.cvc \ - arith-int-002.cvc \ - arith-int-003.cvc \ - arith-int-005.cvc \ - arith-int-006.cvc \ - arith-int-008.cvc \ - arith-int-009.cvc \ - arith-int-010.cvc \ arith-int-014.cvc \ arith-int-015.cvc \ - arith-int-016.cvc \ - arith-int-017.cvc \ - arith-int-018.cvc \ - arith-int-019.cvc \ - arith-int-020.cvc \ arith-int-021.cvc \ arith-int-023.cvc \ arith-int-025.cvc \ - arith-int-026.cvc \ - arith-int-027.cvc \ - arith-int-028.cvc \ - arith-int-029.cvc \ - arith-int-030.cvc \ - arith-int-031.cvc \ - arith-int-032.cvc \ - arith-int-033.cvc \ - arith-int-034.cvc \ - arith-int-035.cvc \ - arith-int-036.cvc \ - arith-int-037.cvc \ - arith-int-038.cvc \ - arith-int-039.cvc \ - arith-int-040.cvc \ - arith-int-041.cvc \ - arith-int-043.cvc \ - arith-int-044.cvc \ - arith-int-045.cvc \ - arith-int-046.cvc \ - arith-int-049.cvc \ - arith-int-051.cvc \ - arith-int-052.cvc \ - arith-int-053.cvc \ - arith-int-054.cvc \ - arith-int-055.cvc \ - arith-int-056.cvc \ - arith-int-057.cvc \ - arith-int-058.cvc \ - arith-int-059.cvc \ - arith-int-060.cvc \ - arith-int-061.cvc \ - arith-int-062.cvc \ - arith-int-063.cvc \ - arith-int-064.cvc \ - arith-int-065.cvc \ - arith-int-066.cvc \ - arith-int-067.cvc \ - arith-int-068.cvc \ - arith-int-069.cvc \ - arith-int-070.cvc \ - arith-int-071.cvc \ - arith-int-072.cvc \ - arith-int-073.cvc \ - arith-int-074.cvc \ - arith-int-075.cvc \ - arith-int-076.cvc \ - arith-int-077.cvc \ - arith-int-078.cvc \ - arith-int-079.cvc \ - arith-int-080.cvc \ - arith-int-081.cvc \ - arith-int-083.cvc \ - arith-int-086.cvc \ - arith-int-087.cvc \ - arith-int-088.cvc \ - arith-int-089.cvc \ - arith-int-090.cvc \ - arith-int-091.cvc \ - arith-int-092.cvc \ - arith-int-093.cvc \ - arith-int-094.cvc \ - arith-int-095.cvc \ - arith-int-096.cvc \ - arith-int-098.cvc \ - arith-int-099.cvc \ - arith-int-100.cvc - -FAILING_TESTS = \ - arith-int-007.cvc \ - arith-int-082.cvc \ - arith-int-098.cvc + arith-int-079.cvc #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/arith/integers/arith-int-001.cvc b/test/regress/regress0/arith/integers/arith-int-001.cvc deleted file mode 100644 index 03ed1a6ae..000000000 --- a/test/regress/regress0/arith/integers/arith-int-001.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-002.cvc b/test/regress/regress0/arith/integers/arith-int-002.cvc deleted file mode 100644 index 849daba79..000000000 --- a/test/regress/regress0/arith/integers/arith-int-002.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-003.cvc b/test/regress/regress0/arith/integers/arith-int-003.cvc deleted file mode 100644 index 9c060c469..000000000 --- a/test/regress/regress0/arith/integers/arith-int-003.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-004.cvc b/test/regress/regress0/arith/integers/arith-int-004.cvc deleted file mode 100644 index 314b76d18..000000000 --- a/test/regress/regress0/arith/integers/arith-int-004.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: invalid - -x0, x1, x2, x3 : INT; -ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ; -ASSERT (9 * x0) + (2 * x1) + (26 * x2) + (-3 * x3) >= 11 ; -ASSERT (3 * x0) + (-29 * x1) + (-4 * x2) + (-17 * x3) > 2 ; -ASSERT (7 * x0) + (-29 * x1) + (12 * x2) + (16 * x3) >= -14 ; -ASSERT (21 * x0) + (32 * x1) + (16 * x2) + (4 * x3) >= -19 ; -ASSERT (6 * x0) + (23 * x1) + (-10 * x2) + (-25 * x3) > 5 ; -ASSERT (-26 * x0) + (4 * x1) + (-23 * x2) + (-30 * x3) >= 25 ; -ASSERT (-4 * x0) + (-13 * x1) + (15 * x2) + (-12 * x3) > -13 ; -ASSERT (-11 * x0) + (31 * x1) + (0 * x2) + (-2 * x3) < 8 ; -ASSERT (7 * x0) + (14 * x1) + (-21 * x2) + (-5 * x3) >= -19 ; -ASSERT (-28 * x0) + (-12 * x1) + (7 * x2) + (-5 * x3) <= 28; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-005.cvc b/test/regress/regress0/arith/integers/arith-int-005.cvc deleted file mode 100644 index 9b9776ad3..000000000 --- a/test/regress/regress0/arith/integers/arith-int-005.cvc +++ /dev/null @@ -1,14 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-006.cvc b/test/regress/regress0/arith/integers/arith-int-006.cvc deleted file mode 100644 index 999b4a5b4..000000000 --- a/test/regress/regress0/arith/integers/arith-int-006.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-007.cvc b/test/regress/regress0/arith/integers/arith-int-007.cvc deleted file mode 100644 index 4cb4d88ef..000000000 --- a/test/regress/regress0/arith/integers/arith-int-007.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-008.cvc b/test/regress/regress0/arith/integers/arith-int-008.cvc deleted file mode 100644 index 1ae22c993..000000000 --- a/test/regress/regress0/arith/integers/arith-int-008.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-009.cvc b/test/regress/regress0/arith/integers/arith-int-009.cvc deleted file mode 100644 index 9bd7a2ce4..000000000 --- a/test/regress/regress0/arith/integers/arith-int-009.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-010.cvc b/test/regress/regress0/arith/integers/arith-int-010.cvc deleted file mode 100644 index 4ac85a984..000000000 --- a/test/regress/regress0/arith/integers/arith-int-010.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-011.cvc b/test/regress/regress0/arith/integers/arith-int-011.cvc deleted file mode 100644 index bd2fa2a0d..000000000 --- a/test/regress/regress0/arith/integers/arith-int-011.cvc +++ /dev/null @@ -1,5 +0,0 @@ -% EXPECT: invalid -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; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-012.cvc b/test/regress/regress0/arith/integers/arith-int-012.cvc deleted file mode 100644 index 11b0dab27..000000000 --- a/test/regress/regress0/arith/integers/arith-int-012.cvc +++ /dev/null @@ -1,5 +0,0 @@ -% EXPECT: invalid -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; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-013.cvc b/test/regress/regress0/arith/integers/arith-int-013.cvc deleted file mode 100644 index 329251cae..000000000 --- a/test/regress/regress0/arith/integers/arith-int-013.cvc +++ /dev/null @@ -1,5 +0,0 @@ -% EXPECT: invalid -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; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-016.cvc b/test/regress/regress0/arith/integers/arith-int-016.cvc deleted file mode 100644 index 6774dd2d1..000000000 --- a/test/regress/regress0/arith/integers/arith-int-016.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-017.cvc b/test/regress/regress0/arith/integers/arith-int-017.cvc deleted file mode 100644 index e9a06125a..000000000 --- a/test/regress/regress0/arith/integers/arith-int-017.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-018.cvc b/test/regress/regress0/arith/integers/arith-int-018.cvc deleted file mode 100644 index 4cb97b77e..000000000 --- a/test/regress/regress0/arith/integers/arith-int-018.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-019.cvc b/test/regress/regress0/arith/integers/arith-int-019.cvc deleted file mode 100644 index cf9ae2d70..000000000 --- a/test/regress/regress0/arith/integers/arith-int-019.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-020.cvc b/test/regress/regress0/arith/integers/arith-int-020.cvc deleted file mode 100644 index 07a827465..000000000 --- a/test/regress/regress0/arith/integers/arith-int-020.cvc +++ /dev/null @@ -1,20 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-022.cvc b/test/regress/regress0/arith/integers/arith-int-022.cvc deleted file mode 100644 index 584348da4..000000000 --- a/test/regress/regress0/arith/integers/arith-int-022.cvc +++ /dev/null @@ -1,4 +0,0 @@ -% EXPECT: invalid -x0, x1, x2, x3 : INT; -ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-024.cvc b/test/regress/regress0/arith/integers/arith-int-024.cvc deleted file mode 100644 index f57136dd1..000000000 --- a/test/regress/regress0/arith/integers/arith-int-024.cvc +++ /dev/null @@ -1,4 +0,0 @@ -% EXPECT: invalid -x0, x1, x2, x3 : INT; -ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-026.cvc b/test/regress/regress0/arith/integers/arith-int-026.cvc deleted file mode 100644 index 9e69aa2d1..000000000 --- a/test/regress/regress0/arith/integers/arith-int-026.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-027.cvc b/test/regress/regress0/arith/integers/arith-int-027.cvc deleted file mode 100644 index b45622fea..000000000 --- a/test/regress/regress0/arith/integers/arith-int-027.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-028.cvc b/test/regress/regress0/arith/integers/arith-int-028.cvc deleted file mode 100644 index 61fee4203..000000000 --- a/test/regress/regress0/arith/integers/arith-int-028.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-029.cvc b/test/regress/regress0/arith/integers/arith-int-029.cvc deleted file mode 100644 index ee49bbb68..000000000 --- a/test/regress/regress0/arith/integers/arith-int-029.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-030.cvc b/test/regress/regress0/arith/integers/arith-int-030.cvc deleted file mode 100644 index 70b6a3785..000000000 --- a/test/regress/regress0/arith/integers/arith-int-030.cvc +++ /dev/null @@ -1,21 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-031.cvc b/test/regress/regress0/arith/integers/arith-int-031.cvc deleted file mode 100644 index 86242f7aa..000000000 --- a/test/regress/regress0/arith/integers/arith-int-031.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-032.cvc b/test/regress/regress0/arith/integers/arith-int-032.cvc deleted file mode 100644 index 1ee4c9844..000000000 --- a/test/regress/regress0/arith/integers/arith-int-032.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-033.cvc b/test/regress/regress0/arith/integers/arith-int-033.cvc deleted file mode 100644 index 599ba4e9a..000000000 --- a/test/regress/regress0/arith/integers/arith-int-033.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-034.cvc b/test/regress/regress0/arith/integers/arith-int-034.cvc deleted file mode 100644 index ec615a785..000000000 --- a/test/regress/regress0/arith/integers/arith-int-034.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-035.cvc b/test/regress/regress0/arith/integers/arith-int-035.cvc deleted file mode 100644 index e7dee2484..000000000 --- a/test/regress/regress0/arith/integers/arith-int-035.cvc +++ /dev/null @@ -1,19 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-036.cvc b/test/regress/regress0/arith/integers/arith-int-036.cvc deleted file mode 100644 index 9594f9586..000000000 --- a/test/regress/regress0/arith/integers/arith-int-036.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-037.cvc b/test/regress/regress0/arith/integers/arith-int-037.cvc deleted file mode 100644 index 4d4422d3f..000000000 --- a/test/regress/regress0/arith/integers/arith-int-037.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-038.cvc b/test/regress/regress0/arith/integers/arith-int-038.cvc deleted file mode 100644 index 476133b24..000000000 --- a/test/regress/regress0/arith/integers/arith-int-038.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-039.cvc b/test/regress/regress0/arith/integers/arith-int-039.cvc deleted file mode 100644 index 9e9235ae8..000000000 --- a/test/regress/regress0/arith/integers/arith-int-039.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-040.cvc b/test/regress/regress0/arith/integers/arith-int-040.cvc deleted file mode 100644 index 68502349f..000000000 --- a/test/regress/regress0/arith/integers/arith-int-040.cvc +++ /dev/null @@ -1,16 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-041.cvc b/test/regress/regress0/arith/integers/arith-int-041.cvc deleted file mode 100644 index a0c2dc0f9..000000000 --- a/test/regress/regress0/arith/integers/arith-int-041.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-043.cvc b/test/regress/regress0/arith/integers/arith-int-043.cvc deleted file mode 100644 index 7efea85e5..000000000 --- a/test/regress/regress0/arith/integers/arith-int-043.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-044.cvc b/test/regress/regress0/arith/integers/arith-int-044.cvc deleted file mode 100644 index f933b014b..000000000 --- a/test/regress/regress0/arith/integers/arith-int-044.cvc +++ /dev/null @@ -1,10 +0,0 @@ -% EXPECT: valid -%%%% 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/regress0/arith/integers/arith-int-045.cvc b/test/regress/regress0/arith/integers/arith-int-045.cvc deleted file mode 100644 index ca1a12ba6..000000000 --- a/test/regress/regress0/arith/integers/arith-int-045.cvc +++ /dev/null @@ -1,9 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-046.cvc b/test/regress/regress0/arith/integers/arith-int-046.cvc deleted file mode 100644 index d4d206c6e..000000000 --- a/test/regress/regress0/arith/integers/arith-int-046.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-047.cvc b/test/regress/regress0/arith/integers/arith-int-047.cvc deleted file mode 100644 index 0763e5dc3..000000000 --- a/test/regress/regress0/arith/integers/arith-int-047.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% EXPECT: invalid -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 ; -ASSERT (-3 * x0) + (-2 * x1) + (26 * x2) + (30 * x3) < -27 ; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-048.cvc b/test/regress/regress0/arith/integers/arith-int-048.cvc deleted file mode 100644 index e7c05332d..000000000 --- a/test/regress/regress0/arith/integers/arith-int-048.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% EXPECT: invalid -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 ; -ASSERT (15 * x0) + (-11 * x1) + (-19 * x2) + (-13 * x3) < 5; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-049.cvc b/test/regress/regress0/arith/integers/arith-int-049.cvc deleted file mode 100644 index 8eabc78a8..000000000 --- a/test/regress/regress0/arith/integers/arith-int-049.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-050.cvc b/test/regress/regress0/arith/integers/arith-int-050.cvc deleted file mode 100644 index f0ba939b7..000000000 --- a/test/regress/regress0/arith/integers/arith-int-050.cvc +++ /dev/null @@ -1,6 +0,0 @@ -% EXPECT: invalid -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 ; -ASSERT (-13 * x0) + (24 * x1) + (27 * x2) + (20 * x3) < -5; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-051.cvc b/test/regress/regress0/arith/integers/arith-int-051.cvc deleted file mode 100644 index 9a2497432..000000000 --- a/test/regress/regress0/arith/integers/arith-int-051.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-052.cvc b/test/regress/regress0/arith/integers/arith-int-052.cvc deleted file mode 100644 index 83fdc89c8..000000000 --- a/test/regress/regress0/arith/integers/arith-int-052.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-053.cvc b/test/regress/regress0/arith/integers/arith-int-053.cvc deleted file mode 100644 index fa38fa3da..000000000 --- a/test/regress/regress0/arith/integers/arith-int-053.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-054.cvc b/test/regress/regress0/arith/integers/arith-int-054.cvc deleted file mode 100644 index 9b0066966..000000000 --- a/test/regress/regress0/arith/integers/arith-int-054.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-055.cvc b/test/regress/regress0/arith/integers/arith-int-055.cvc deleted file mode 100644 index 9729fb565..000000000 --- a/test/regress/regress0/arith/integers/arith-int-055.cvc +++ /dev/null @@ -1,12 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-056.cvc b/test/regress/regress0/arith/integers/arith-int-056.cvc deleted file mode 100644 index e1c3ee1da..000000000 --- a/test/regress/regress0/arith/integers/arith-int-056.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-057.cvc b/test/regress/regress0/arith/integers/arith-int-057.cvc deleted file mode 100644 index 4e7b939b4..000000000 --- a/test/regress/regress0/arith/integers/arith-int-057.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-058.cvc b/test/regress/regress0/arith/integers/arith-int-058.cvc deleted file mode 100644 index 4d964f1c6..000000000 --- a/test/regress/regress0/arith/integers/arith-int-058.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-059.cvc b/test/regress/regress0/arith/integers/arith-int-059.cvc deleted file mode 100644 index 841d9c8e1..000000000 --- a/test/regress/regress0/arith/integers/arith-int-059.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-060.cvc b/test/regress/regress0/arith/integers/arith-int-060.cvc deleted file mode 100644 index 227cb49b1..000000000 --- a/test/regress/regress0/arith/integers/arith-int-060.cvc +++ /dev/null @@ -1,15 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-061.cvc b/test/regress/regress0/arith/integers/arith-int-061.cvc deleted file mode 100644 index 4a3cc28d0..000000000 --- a/test/regress/regress0/arith/integers/arith-int-061.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-062.cvc b/test/regress/regress0/arith/integers/arith-int-062.cvc deleted file mode 100644 index f9a3156a2..000000000 --- a/test/regress/regress0/arith/integers/arith-int-062.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-063.cvc b/test/regress/regress0/arith/integers/arith-int-063.cvc deleted file mode 100644 index d88104688..000000000 --- a/test/regress/regress0/arith/integers/arith-int-063.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-064.cvc b/test/regress/regress0/arith/integers/arith-int-064.cvc deleted file mode 100644 index 21ca822e1..000000000 --- a/test/regress/regress0/arith/integers/arith-int-064.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-065.cvc b/test/regress/regress0/arith/integers/arith-int-065.cvc deleted file mode 100644 index b1b9e1b51..000000000 --- a/test/regress/regress0/arith/integers/arith-int-065.cvc +++ /dev/null @@ -1,23 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-066.cvc b/test/regress/regress0/arith/integers/arith-int-066.cvc deleted file mode 100644 index 9532b4198..000000000 --- a/test/regress/regress0/arith/integers/arith-int-066.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-067.cvc b/test/regress/regress0/arith/integers/arith-int-067.cvc deleted file mode 100644 index 5d7b52e69..000000000 --- a/test/regress/regress0/arith/integers/arith-int-067.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-068.cvc b/test/regress/regress0/arith/integers/arith-int-068.cvc deleted file mode 100644 index 107a21a12..000000000 --- a/test/regress/regress0/arith/integers/arith-int-068.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-069.cvc b/test/regress/regress0/arith/integers/arith-int-069.cvc deleted file mode 100644 index 3fab229b0..000000000 --- a/test/regress/regress0/arith/integers/arith-int-069.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-070.cvc b/test/regress/regress0/arith/integers/arith-int-070.cvc deleted file mode 100644 index cd828da5f..000000000 --- a/test/regress/regress0/arith/integers/arith-int-070.cvc +++ /dev/null @@ -1,17 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-071.cvc b/test/regress/regress0/arith/integers/arith-int-071.cvc deleted file mode 100644 index ce5336476..000000000 --- a/test/regress/regress0/arith/integers/arith-int-071.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-072.cvc b/test/regress/regress0/arith/integers/arith-int-072.cvc deleted file mode 100644 index 10222deae..000000000 --- a/test/regress/regress0/arith/integers/arith-int-072.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-073.cvc b/test/regress/regress0/arith/integers/arith-int-073.cvc deleted file mode 100644 index 98e74be8f..000000000 --- a/test/regress/regress0/arith/integers/arith-int-073.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-074.cvc b/test/regress/regress0/arith/integers/arith-int-074.cvc deleted file mode 100644 index 28cc48186..000000000 --- a/test/regress/regress0/arith/integers/arith-int-074.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-075.cvc b/test/regress/regress0/arith/integers/arith-int-075.cvc deleted file mode 100644 index 3b5131e8b..000000000 --- a/test/regress/regress0/arith/integers/arith-int-075.cvc +++ /dev/null @@ -1,18 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-076.cvc b/test/regress/regress0/arith/integers/arith-int-076.cvc deleted file mode 100644 index 2c8de7cdf..000000000 --- a/test/regress/regress0/arith/integers/arith-int-076.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-077.cvc b/test/regress/regress0/arith/integers/arith-int-077.cvc deleted file mode 100644 index d14da386e..000000000 --- a/test/regress/regress0/arith/integers/arith-int-077.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-078.cvc b/test/regress/regress0/arith/integers/arith-int-078.cvc deleted file mode 100644 index 3197c6524..000000000 --- a/test/regress/regress0/arith/integers/arith-int-078.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-080.cvc b/test/regress/regress0/arith/integers/arith-int-080.cvc deleted file mode 100644 index 8be0f9a73..000000000 --- a/test/regress/regress0/arith/integers/arith-int-080.cvc +++ /dev/null @@ -1,11 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-081.cvc b/test/regress/regress0/arith/integers/arith-int-081.cvc deleted file mode 100644 index 546148376..000000000 --- a/test/regress/regress0/arith/integers/arith-int-081.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-082.cvc b/test/regress/regress0/arith/integers/arith-int-082.cvc deleted file mode 100644 index 62bd45de7..000000000 --- a/test/regress/regress0/arith/integers/arith-int-082.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-083.cvc b/test/regress/regress0/arith/integers/arith-int-083.cvc deleted file mode 100644 index 6b1084353..000000000 --- a/test/regress/regress0/arith/integers/arith-int-083.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-084.cvc b/test/regress/regress0/arith/integers/arith-int-084.cvc deleted file mode 100644 index 5f0e17afe..000000000 --- a/test/regress/regress0/arith/integers/arith-int-084.cvc +++ /dev/null @@ -1,7 +0,0 @@ -% EXPECT: invalid -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 ; -ASSERT (-31 * x0) + (23 * x1) + (4 * x2) + (29 * x3) > -6 ; -ASSERT (-14 * x0) + (32 * x1) + (-8 * x2) + (-8 * x3) <= -1; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-085.cvc b/test/regress/regress0/arith/integers/arith-int-085.cvc deleted file mode 100644 index 74dd714e8..000000000 --- a/test/regress/regress0/arith/integers/arith-int-085.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% EXPECT: invalid -%% down from 3 -x0, x1, x2, x3 : INT; -ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ; -ASSERT (-9 * x0) + (30 * x1) + (-17 * x2) + (29 * x3) >= -15 ; -ASSERT (21 * x0) + (29 * x1) + (12 * x2) + (-3 * x3) <= -21 ; -ASSERT (-16 * x0) + (-26 * x1) + (11 * x2) + (-12 * x3) >= -14; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-086.cvc b/test/regress/regress0/arith/integers/arith-int-086.cvc deleted file mode 100644 index 64c212b3c..000000000 --- a/test/regress/regress0/arith/integers/arith-int-086.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-087.cvc b/test/regress/regress0/arith/integers/arith-int-087.cvc deleted file mode 100644 index 312c08917..000000000 --- a/test/regress/regress0/arith/integers/arith-int-087.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-088.cvc b/test/regress/regress0/arith/integers/arith-int-088.cvc deleted file mode 100644 index 5212640be..000000000 --- a/test/regress/regress0/arith/integers/arith-int-088.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-089.cvc b/test/regress/regress0/arith/integers/arith-int-089.cvc deleted file mode 100644 index 7ff36d29e..000000000 --- a/test/regress/regress0/arith/integers/arith-int-089.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-090.cvc b/test/regress/regress0/arith/integers/arith-int-090.cvc deleted file mode 100644 index 52b9c13f0..000000000 --- a/test/regress/regress0/arith/integers/arith-int-090.cvc +++ /dev/null @@ -1,13 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-091.cvc b/test/regress/regress0/arith/integers/arith-int-091.cvc deleted file mode 100644 index 29a19db39..000000000 --- a/test/regress/regress0/arith/integers/arith-int-091.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-092.cvc b/test/regress/regress0/arith/integers/arith-int-092.cvc deleted file mode 100644 index 51c8a6bc4..000000000 --- a/test/regress/regress0/arith/integers/arith-int-092.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-093.cvc b/test/regress/regress0/arith/integers/arith-int-093.cvc deleted file mode 100644 index 7d2123d41..000000000 --- a/test/regress/regress0/arith/integers/arith-int-093.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-094.cvc b/test/regress/regress0/arith/integers/arith-int-094.cvc deleted file mode 100644 index a5f1aefce..000000000 --- a/test/regress/regress0/arith/integers/arith-int-094.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-095.cvc b/test/regress/regress0/arith/integers/arith-int-095.cvc deleted file mode 100644 index bc47d6f49..000000000 --- a/test/regress/regress0/arith/integers/arith-int-095.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: valid -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/regress0/arith/integers/arith-int-096.cvc b/test/regress/regress0/arith/integers/arith-int-096.cvc deleted file mode 100644 index 2f6cf3155..000000000 --- a/test/regress/regress0/arith/integers/arith-int-096.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-097.cvc b/test/regress/regress0/arith/integers/arith-int-097.cvc deleted file mode 100644 index b05061192..000000000 --- a/test/regress/regress0/arith/integers/arith-int-097.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% EXPECT: invalid -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 ; -ASSERT (-8 * x0) + (-1 * x1) + (-25 * x2) + (-7 * x3) <= -31 ; -ASSERT (-7 * x0) + (11 * x1) + (-5 * x2) + (-19 * x3) > 32 ; -ASSERT (-22 * x0) + (13 * x1) + (-16 * x2) + (-12 * x3) <= 32; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-098.cvc b/test/regress/regress0/arith/integers/arith-int-098.cvc deleted file mode 100644 index 08cfd9c9c..000000000 --- a/test/regress/regress0/arith/integers/arith-int-098.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% EXPECT: invalid -x0, x1, x2, x3 : INT; -ASSERT (-28 * x0) + (12 * x1) + (-19 * x2) + (10 * x3) = 16 ; -ASSERT (19 * x0) + (-25 * x1) + (-8 * x2) + (-32 * x3) = 12; -ASSERT (18 * x0) + (21 * x1) + (5 * x2) + (-14 * x3) < -12 ; -ASSERT (-13 * x0) + (32 * x1) + (-5 * x2) + (-13 * x3) <= -15 ; -ASSERT (30 * x0) + (-19 * x1) + (28 * x2) + (-27 * x3) <= -18 ; -QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-099.cvc b/test/regress/regress0/arith/integers/arith-int-099.cvc deleted file mode 100644 index 0d74dcb39..000000000 --- a/test/regress/regress0/arith/integers/arith-int-099.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% EXPECT: invalid -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/regress0/arith/integers/arith-int-100.cvc b/test/regress/regress0/arith/integers/arith-int-100.cvc deleted file mode 100644 index 7e07bee14..000000000 --- a/test/regress/regress0/arith/integers/arith-int-100.cvc +++ /dev/null @@ -1,8 +0,0 @@ -% EXPECT: invalid -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; |