diff options
Diffstat (limited to 'test/regress/regress0/arith/integers')
104 files changed, 1604 insertions, 0 deletions
diff --git a/test/regress/regress0/arith/integers/Makefile b/test/regress/regress0/arith/integers/Makefile new file mode 100644 index 000000000..4144299bd --- /dev/null +++ b/test/regress/regress0/arith/integers/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../../.. +srcdir = test/regress/regress0/arith/integers + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am new file mode 100644 index 000000000..3d7f40c71 --- /dev/null +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -0,0 +1,130 @@ +SUBDIRS = . + +TESTS_ENVIRONMENT = @srcdir@/../../../run_regression @top_builddir@/src/main/cvc4 +MAKEFLAGS = -k + +# These are run for all build profiles. +# If a test shouldn't be run in e.g. competition mode, +# put it below in "TESTS +=" +TESTS = \ + arith-int-001.cvc \ + arith-int-002.cvc \ + arith-int-003.cvc \ + arith-int-004.cvc \ + arith-int-005.cvc \ + arith-int-006.cvc \ + arith-int-007.cvc \ + arith-int-009.cvc \ + arith-int-010.cvc \ + arith-int-011.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-024.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-044.cvc \ + arith-int-045.cvc \ + arith-int-046.cvc \ + arith-int-048.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-085.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-099.cvc + +EXTRA_DIST = $(TESTS) \ + arith-int-008.cvc \ + arith-int-012.cvc \ + arith-int-013.cvc \ + arith-int-022.cvc \ + arith-int-042.cvc \ + arith-int-042.min.cvc \ + arith-int-043.cvc \ + arith-int-047.cvc \ + arith-int-050.cvc \ + arith-int-082.cvc \ + arith-int-084.cvc \ + arith-int-097.cvc \ + arith-int-098.cvc \ + arith-int-100.cvc + +#if CVC4_BUILD_PROFILE_COMPETITION +#else +#TESTS += \ +# error.cvc +#endif +# +# and make sure to distribute it +#EXTRA_DIST += \ +# error.cvc + +# synonyms for "check" in this directory +.PHONY: regress regress0 test +regress regress0 test: check + +# do nothing in this subdir +.PHONY: regress1 regress2 regress3 +regress1 regress2 regress3: diff --git a/test/regress/regress0/arith/integers/arith-int-001.cvc b/test/regress/regress0/arith/integers/arith-int-001.cvc new file mode 100644 index 000000000..8b559dc7f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-001.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..41113ea2f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-002.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..a76f82c56 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-003.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..78d10d4b2 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-004.cvc @@ -0,0 +1,16 @@ +% EXPECT: invalid +% EXIT: 10 + +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 new file mode 100644 index 000000000..b2b1f9bf9 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-005.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..cba51db21 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-006.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..bc49f9688 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-007.cvc @@ -0,0 +1,11 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..a524b86b0 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-008.cvc @@ -0,0 +1,11 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..ccb522d37 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-009.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..832f4e63a --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-010.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..d0cc2e501 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-011.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..46127d24f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-012.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..e018d7a15 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-013.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +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-014.cvc b/test/regress/regress0/arith/integers/arith-int-014.cvc new file mode 100644 index 000000000..75991b051 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-014.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (10 * x0) + (25 * x1) + (10 * x2) + (-28 * x3) <= 20 ; +ASSERT (24 * x0) + (-9 * x1) + (-12 * x2) + (15 * x3) <= 3; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-015.cvc b/test/regress/regress0/arith/integers/arith-int-015.cvc new file mode 100644 index 000000000..00ecbcde2 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-015.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-22 * x0) + (-3 * x1) + (9 * x2) + (-13 * x3) > -31 ; +ASSERT (31 * x0) + (-17 * x1) + (28 * x2) + (-16 * x3) > -28; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-016.cvc b/test/regress/regress0/arith/integers/arith-int-016.cvc new file mode 100644 index 000000000..d01b6c51a --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-016.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..2fee71829 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-017.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..c25f8e784 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-018.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..661eb288b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-019.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..9c6bf3932 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-020.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +% EXIT: 20 +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-021.cvc b/test/regress/regress0/arith/integers/arith-int-021.cvc new file mode 100644 index 000000000..bfcf022f5 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-021.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (8 * x0) + (-27 * x1) + (29 * x2) + (-13 * x3) < 12; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-022.cvc b/test/regress/regress0/arith/integers/arith-int-022.cvc new file mode 100644 index 000000000..4a439cdb1 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-022.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +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-023.cvc b/test/regress/regress0/arith/integers/arith-int-023.cvc new file mode 100644 index 000000000..fa161b2d9 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-023.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (29 * x0) + (-19 * x1) + (23 * x2) + (15 * x3) <= 9; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-024.cvc b/test/regress/regress0/arith/integers/arith-int-024.cvc new file mode 100644 index 000000000..c4af43db4 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-024.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +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-025.cvc b/test/regress/regress0/arith/integers/arith-int-025.cvc new file mode 100644 index 000000000..8d527322d --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-025.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +% EXIT: 10 +x0, x1, x2, x3 : INT; +ASSERT (-19 * x0) + (-29 * x1) + (2 * x2) + (26 * x3) >= 3; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-026.cvc b/test/regress/regress0/arith/integers/arith-int-026.cvc new file mode 100644 index 000000000..b08a4e852 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-026.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..811726726 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-027.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..49562ad73 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-028.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..1e8687ec3 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-029.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..1ead5e5a4 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-030.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..3eac975fe --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-031.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..0128c4dbd --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-032.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..9dda4dbf8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-033.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..b8f4dd5f8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-034.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..6adae83fe --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-035.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..94074b8e1 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-036.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..5ad2acd37 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-037.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..807ea029b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-038.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..3ee88fe80 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-039.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..5484f7dde --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-040.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..a3d8889b2 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-041.cvc @@ -0,0 +1,10 @@ +% EXPECT: invalid +% EXIT: 10 +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-042.cvc b/test/regress/regress0/arith/integers/arith-int-042.cvc new file mode 100644 index 000000000..df9314482 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-042.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (-9 * x0) + (25 * x1) + (0 * x2) + (13 * x3) = 17 ; +ASSERT (-6 * x0) + (32 * x1) + (2 * x2) + (-32 * x3) = -5 ; +ASSERT (19 * x0) + (25 * x1) + (-32 * x2) + (-29 * x3) <= 14 ; +ASSERT (6 * x0) + (22 * x1) + (-24 * x2) + (-6 * x3) < -21 ; +ASSERT (-18 * x0) + (-21 * x1) + (-29 * x2) + (12 * x3) > 17 ; +ASSERT (-25 * x0) + (-5 * x1) + (-22 * x2) + (-7 * x3) > -21; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-042.min.cvc b/test/regress/regress0/arith/integers/arith-int-042.min.cvc new file mode 100644 index 000000000..e19bdda0e --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-042.min.cvc @@ -0,0 +1,5 @@ +% EXPECT: valid +% EXIT: 20 +x1: INT; +x0: INT; +QUERY NOT (((x0 * 6) + (x1 * 32)) = 1); diff --git a/test/regress/regress0/arith/integers/arith-int-043.cvc b/test/regress/regress0/arith/integers/arith-int-043.cvc new file mode 100644 index 000000000..53f0e9903 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-043.cvc @@ -0,0 +1,10 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..b42affada --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-044.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +% EXIT: 20 +%%%% 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 new file mode 100644 index 000000000..f70eff09a --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-045.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..ec694ad2b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-046.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..b5f4cb3a8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-047.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..76fa395bc --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-048.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..b415776e8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-049.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..d35f445d8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-050.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..8a696d2de --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-051.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..ae7e2c15f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-052.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..3cd2f3df6 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-053.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..95eb7a6d6 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-054.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..6ed1bf4cd --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-055.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..028c1979b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-056.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..1984622c3 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-057.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..c6c87c64b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-058.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..558789493 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-059.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..75968a935 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-060.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..68f54742c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-061.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..1c1c54b07 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-062.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..77843cbc3 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-063.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..0c6847c61 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-064.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..64fe7fd49 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-065.cvc @@ -0,0 +1,24 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..6c7035ded --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-066.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..fc74cc94c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-067.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..d4360159f --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-068.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..f877d3108 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-069.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..65e2fd6d8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-070.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..e8b7a206c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-071.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..7670bb468 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-072.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..0b0f6b76c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-073.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..1f6578d09 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-074.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..e6f136797 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-075.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..d0d2bbd59 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-076.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..4f2985da8 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-077.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..d65638290 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-078.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +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-079.cvc b/test/regress/regress0/arith/integers/arith-int-079.cvc new file mode 100644 index 000000000..83a24f245 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-079.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +x0, x1, x2, x3 : INT; +ASSERT (6 * x0) + (2 * x1) + (22 * x2) + (-18 * x3) = -15 ; +ASSERT (-8 * x0) + (-25 * x1) + (-25 * x2) + (7 * x3) > 10 ; +ASSERT (8 * x0) + (25 * x1) + (-7 * x2) + (-29 * x3) < -25 ; +ASSERT (27 * x0) + (17 * x1) + (-24 * x2) + (-5 * x3) <= 13 ; +ASSERT (5 * x0) + (-3 * x1) + (0 * x2) + (4 * x3) < -26 ; +ASSERT (25 * x0) + (7 * x1) + (27 * x2) + (-14 * x3) < 30 ; +ASSERT (-22 * x0) + (-17 * x1) + (9 * x2) + (-20 * x3) < -19 ; +ASSERT (31 * x0) + (-16 * x1) + (0 * x2) + (6 * x3) >= 18; +QUERY FALSE; diff --git a/test/regress/regress0/arith/integers/arith-int-080.cvc b/test/regress/regress0/arith/integers/arith-int-080.cvc new file mode 100644 index 000000000..f29f91896 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-080.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..fcf857e29 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-081.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..0fbeeb03b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-082.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..90171f772 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-083.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..f190c5d4d --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-084.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..281ba0e29 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-085.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +%% 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 new file mode 100644 index 000000000..21c058f7c --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-086.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..c403fdf3e --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-087.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..04361f9b1 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-088.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..5d7b9e2d2 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-089.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..a9f4b03a4 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-090.cvc @@ -0,0 +1,14 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..ebf728533 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-091.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..f6622eb0b --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-092.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..3cb1aed11 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-093.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..4abce2679 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-094.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..3aa4b2489 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-095.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +% EXIT: 20 +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 new file mode 100644 index 000000000..f409f37af --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-096.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..f0fca22fb --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-097.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..37a472265 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-098.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..9ff8724af --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-099.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +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 new file mode 100644 index 000000000..a75128232 --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-int-100.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +% EXIT: 10 +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; diff --git a/test/regress/regress0/arith/integers/arith-interval.cvc b/test/regress/regress0/arith/integers/arith-interval.cvc new file mode 100644 index 000000000..e8b229faa --- /dev/null +++ b/test/regress/regress0/arith/integers/arith-interval.cvc @@ -0,0 +1,8 @@ +% EXPECT: valid +% EXIT: 20 +x: INT; +P: INT -> BOOLEAN; + +ASSERT 1 <= x AND x <= 2; +ASSERT P(1) AND P(2); +QUERY P(x); |