diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-15 15:31:48 -0600 |
|---|---|---|
| committer | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-15 13:31:48 -0800 |
| commit | 55037e0bcef45c795f28ff3fcf6c1055af465c70 (patch) | |
| tree | 397d89bd10e541e1206c5dafdb8cf731feb34730 /test/regress/regress1/arith | |
| parent | 52a39aca19b7238d08c3cebcfa46436a73194008 (diff) | |
Refactor regressions (#1581)
Diffstat (limited to 'test/regress/regress1/arith')
105 files changed, 2257 insertions, 0 deletions
diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am new file mode 100644 index 000000000..e2b0e93d9 --- /dev/null +++ b/test/regress/regress1/arith/Makefile.am @@ -0,0 +1,139 @@ +# don't override a BINARY imported from a personal.mk +@mk_if@eq ($(BINARY),) +@mk_empty@BINARY = cvc4 +end@mk_if@ + +LOG_COMPILER = @srcdir@/../../run_regression +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) + +if AUTOMAKE_1_11 +# old-style (pre-automake 1.12) test harness +TESTS_ENVIRONMENT = \ + $(LOG_COMPILER) \ + $(AM_LOG_FLAGS) $(LOG_FLAGS) +endif + +# 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-004.cvc \ + arith-int-011.cvc \ + arith-int-048.cvc \ + arith-int-050.cvc \ + arith-int-084.cvc \ + arith-int-085.cvc \ + arith-int-097.cvc \ + bug716.0.smt2 \ + problem__003.smt2 \ + bug547.1.smt2 \ + bug716.1.cvc \ + div.03.smt2 \ + div.06.smt2 \ + div.08.smt2 \ + div.09.smt2 \ + miplib3.cvc \ + mod.02.smt2 \ + mod.03.smt2 \ + mult.02.smt2 \ + arith-int-012.cvc \ + arith-int-013.cvc \ + arith-int-022.cvc \ + arith-int-024.cvc \ + arith-int-047.cvc + +EXTRA_DIST = $(TESTS) \ + arith-int-008.cvc \ + arith-int-018.cvc \ + arith-int-020.cvc \ + arith-int-026.cvc \ + arith-int-029.cvc \ + arith-int-030.cvc \ + arith-int-043.cvc \ + arith-int-044.cvc \ + arith-int-049.cvc \ + arith-int-061.cvc \ + arith-int-062.cvc \ + arith-int-064.cvc \ + arith-int-065.cvc \ + arith-int-081.cvc \ + arith-int-083.cvc \ + arith-int-090.cvc \ + arith-int-091.cvc \ + arith-int-092.cvc \ + arith-int-094.cvc \ + arith-int-096.cvc \ + arith-int-098.cvc \ + arith-int-001.cvc \ + arith-int-002.cvc \ + arith-int-003.cvc \ + arith-int-005.cvc \ + arith-int-006.cvc \ + arith-int-009.cvc \ + arith-int-010.cvc \ + arith-int-016.cvc \ + arith-int-017.cvc \ + arith-int-019.cvc \ + arith-int-027.cvc \ + arith-int-028.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-045.cvc \ + arith-int-046.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-063.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-080.cvc \ + arith-int-086.cvc \ + arith-int-087.cvc \ + arith-int-088.cvc \ + arith-int-089.cvc \ + arith-int-093.cvc \ + arith-int-095.cvc \ + arith-int-099.cvc \ + arith-int-100.cvc + +FAILING_TESTS = \ + arith-int-007.cvc \ + arith-int-082.cvc \ + arith-int-098.cvc + +EXTRA_DIST = $(TESTS) + +# synonyms for "check" in this directory +.PHONY: regress regress1 test +regress regress1 test: check + +# do nothing in this subdir +.PHONY: regress0 regress2 regress3 regress4 +regress0 regress2 regress3 regress4: diff --git a/test/regress/regress1/arith/arith-int-001.cvc b/test/regress/regress1/arith/arith-int-001.cvc new file mode 100644 index 000000000..03ed1a6ae --- /dev/null +++ b/test/regress/regress1/arith/arith-int-001.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-23 * x0) + (-23 * x1) + (5 * x2) + (-17 * x3) = 7 ; +ASSERT (-14 * x0) + (-14 * x1) + (19 * x2) + (-24 * x3) = 29 ; +ASSERT (-16 * x0) + (-17 * x1) + (8 * x2) + (4 * x3) > -10 ; +ASSERT (6 * x0) + (-10 * x1) + (-22 * x2) + (-22 * x3) >= 0 ; +ASSERT (18 * x0) + (0 * x1) + (27 * x2) + (7 * x3) <= -2 ; +ASSERT (-23 * x0) + (27 * x1) + (24 * x2) + (-23 * x3) > -25 ; +ASSERT (3 * x0) + (32 * x1) + (15 * x2) + (-21 * x3) >= -10 ; +ASSERT (-27 * x0) + (-16 * x1) + (21 * x2) + (-2 * x3) < 30 ; +ASSERT (-25 * x0) + (-18 * x1) + (-23 * x2) + (22 * x3) < -15 ; +ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (-26 * x3) >= 15 ; +ASSERT (-8 * x0) + (32 * x1) + (9 * x2) + (17 * x3) > -26; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-002.cvc b/test/regress/regress1/arith/arith-int-002.cvc new file mode 100644 index 000000000..849daba79 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-002.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (17 * x0) + (-23 * x1) + (2 * x2) + (-19 * x3) = -18 ; +ASSERT (25 * x0) + (23 * x1) + (21 * x2) + (20 * x3) = 2 ; +ASSERT (-24 * x0) + (-30 * x1) + (-14 * x2) + (13 * x3) <= 15 ; +ASSERT (-26 * x0) + (7 * x1) + (8 * x2) + (14 * x3) <= 16 ; +ASSERT (-1 * x0) + (-3 * x1) + (-19 * x2) + (26 * x3) <= -15 ; +ASSERT (31 * x0) + (19 * x1) + (-19 * x2) + (24 * x3) < -25 ; +ASSERT (8 * x0) + (-27 * x1) + (22 * x2) + (-20 * x3) < -30 ; +ASSERT (25 * x0) + (7 * x1) + (-18 * x2) + (-18 * x3) >= -31 ; +ASSERT (7 * x0) + (-22 * x1) + (-8 * x2) + (-6 * x3) >= -17 ; +ASSERT (-23 * x0) + (14 * x1) + (23 * x2) + (22 * x3) > -29 ; +ASSERT (-6 * x0) + (-6 * x1) + (-19 * x2) + (-4 * x3) > -5; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-003.cvc b/test/regress/regress1/arith/arith-int-003.cvc new file mode 100644 index 000000000..9c060c469 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-003.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (17 * x0) + (-7 * x1) + (15 * x2) + (21 * x3) = 19 ; +ASSERT (6 * x0) + (-24 * x1) + (25 * x2) + (-18 * x3) > -25 ; +ASSERT (-26 * x0) + (-28 * x1) + (-23 * x2) + (0 * x3) < -14 ; +ASSERT (-12 * x0) + (16 * x1) + (26 * x2) + (-23 * x3) <= 11 ; +ASSERT (14 * x0) + (6 * x1) + (9 * x2) + (-29 * x3) > 24 ; +ASSERT (5 * x0) + (-10 * x1) + (21 * x2) + (-26 * x3) > -12 ; +ASSERT (31 * x0) + (6 * x1) + (30 * x2) + (10 * x3) <= -25 ; +ASSERT (-18 * x0) + (-25 * x1) + (-24 * x2) + (-30 * x3) >= -18 ; +ASSERT (29 * x0) + (25 * x1) + (29 * x2) + (-31 * x3) < 6 ; +ASSERT (21 * x0) + (-27 * x1) + (-28 * x2) + (-15 * x3) >= 25 ; +ASSERT (-13 * x0) + (10 * x1) + (-7 * x2) + (-10 * x3) <= -4; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-004.cvc b/test/regress/regress1/arith/arith-int-004.cvc new file mode 100644 index 000000000..314b76d18 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-004.cvc @@ -0,0 +1,15 @@ +% EXPECT: invalid + +x0, x1, x2, x3 : INT; +ASSERT (12 * x0) + (-25 * x1) + (21 * x2) + (7 * x3) < 27 ; +ASSERT (9 * x0) + (2 * x1) + (26 * x2) + (-3 * x3) >= 11 ; +ASSERT (3 * x0) + (-29 * x1) + (-4 * x2) + (-17 * x3) > 2 ; +ASSERT (7 * x0) + (-29 * x1) + (12 * x2) + (16 * x3) >= -14 ; +ASSERT (21 * x0) + (32 * x1) + (16 * x2) + (4 * x3) >= -19 ; +ASSERT (6 * x0) + (23 * x1) + (-10 * x2) + (-25 * x3) > 5 ; +ASSERT (-26 * x0) + (4 * x1) + (-23 * x2) + (-30 * x3) >= 25 ; +ASSERT (-4 * x0) + (-13 * x1) + (15 * x2) + (-12 * x3) > -13 ; +ASSERT (-11 * x0) + (31 * x1) + (0 * x2) + (-2 * x3) < 8 ; +ASSERT (7 * x0) + (14 * x1) + (-21 * x2) + (-5 * x3) >= -19 ; +ASSERT (-28 * x0) + (-12 * x1) + (7 * x2) + (-5 * x3) <= 28; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-005.cvc b/test/regress/regress1/arith/arith-int-005.cvc new file mode 100644 index 000000000..9b9776ad3 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-005.cvc @@ -0,0 +1,14 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (13 * x0) + (0 * x1) + (6 * x2) + (-30 * x3) = -16 ; +ASSERT (-4 * x0) + (-8 * x1) + (14 * x2) + (-8 * x3) = -11 ; +ASSERT (-23 * x0) + (-26 * x1) + (4 * x2) + (-6 * x3) <= -2 ; +ASSERT (-22 * x0) + (-18 * x1) + (-23 * x2) + (5 * x3) < -32 ; +ASSERT (27 * x0) + (-12 * x1) + (-19 * x2) + (-17 * x3) <= -29 ; +ASSERT (12 * x0) + (21 * x1) + (-22 * x2) + (15 * x3) > 4 ; +ASSERT (-15 * x0) + (16 * x1) + (2 * x2) + (-14 * x3) >= -26 ; +ASSERT (4 * x0) + (4 * x1) + (-21 * x2) + (10 * x3) >= -6 ; +ASSERT (-6 * x0) + (25 * x1) + (-14 * x2) + (8 * x3) >= -31 ; +ASSERT (-23 * x0) + (2 * x1) + (-9 * x2) + (19 * x3) <= 10 ; +ASSERT (21 * x0) + (24 * x1) + (14 * x2) + (-6 * x3) <= 0; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-006.cvc b/test/regress/regress1/arith/arith-int-006.cvc new file mode 100644 index 000000000..999b4a5b4 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-006.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-7 * x0) + (-28 * x1) + (8 * x2) + (29 * x3) = -18 ; +ASSERT (11 * x0) + (2 * x1) + (4 * x2) + (23 * x3) = 6 ; +ASSERT (24 * x0) + (-20 * x1) + (23 * x2) + (-2 * x3) = 19 ; +ASSERT (17 * x0) + (-6 * x1) + (2 * x2) + (-22 * x3) = -31 ; +ASSERT (16 * x0) + (-7 * x1) + (27 * x2) + (17 * x3) = -8; +ASSERT (-5 * x0) + (18 * x1) + (3 * x2) + (-1 * x3) <= 29 ; +ASSERT (9 * x0) + (29 * x1) + (30 * x2) + (23 * x3) >= 21 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-007.cvc b/test/regress/regress1/arith/arith-int-007.cvc new file mode 100644 index 000000000..4cb4d88ef --- /dev/null +++ b/test/regress/regress1/arith/arith-int-007.cvc @@ -0,0 +1,10 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-19 * x0) + (17 * x1) + (30 * x2) + (-31 * x3) <= -20 ; +ASSERT (-3 * x0) + (16 * x1) + (20 * x2) + (-25 * x3) < 28 ; +ASSERT (11 * x0) + (13 * x1) + (-15 * x2) + (-8 * x3) <= 18 ; +ASSERT (-21 * x0) + (0 * x1) + (32 * x2) + (7 * x3) > -31 ; +ASSERT (16 * x0) + (24 * x1) + (8 * x2) + (23 * x3) <= 16 ; +ASSERT (25 * x0) + (-11 * x1) + (-8 * x2) + (14 * x3) <= 17 ; +ASSERT (16 * x0) + (-25 * x1) + (-1 * x2) + (13 * x3) < -26; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-008.cvc b/test/regress/regress1/arith/arith-int-008.cvc new file mode 100644 index 000000000..1ae22c993 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-008.cvc @@ -0,0 +1,10 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-12 * x0) + (-15 * x1) + (-31 * x2) + (17 * x3) = -16 ; +ASSERT (11 * x0) + (-5 * x1) + (-8 * x2) + (-17 * x3) > -4 ; +ASSERT (-12 * x0) + (-22 * x1) + (9 * x2) + (-20 * x3) >= 32 ; +ASSERT (24 * x0) + (-32 * x1) + (5 * x2) + (31 * x3) > 20 ; +ASSERT (-30 * x0) + (-4 * x1) + (-4 * x2) + (0 * x3) >= -20 ; +ASSERT (-10 * x0) + (18 * x1) + (17 * x2) + (20 * x3) <= 30 ; +ASSERT (12 * x0) + (-13 * x1) + (4 * x2) + (-27 * x3) > 3; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-009.cvc b/test/regress/regress1/arith/arith-int-009.cvc new file mode 100644 index 000000000..9bd7a2ce4 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-009.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-16 * x0) + (-21 * x1) + (32 * x2) + (32 * x3) = -19 ; +ASSERT (-10 * x0) + (-21 * x1) + (13 * x2) + (-7 * x3) = 2 ; +ASSERT (11 * x0) + (15 * x1) + (-8 * x2) + (-24 * x3) = 29 ; +ASSERT (3 * x0) + (-28 * x1) + (-14 * x2) + (-18 * x3) < 5 ; +ASSERT (-18 * x0) + (-13 * x1) + (25 * x2) + (22 * x3) <= -24 ; +ASSERT (-16 * x0) + (-17 * x1) + (-27 * x2) + (4 * x3) >= -5 ; +ASSERT (21 * x0) + (13 * x1) + (20 * x2) + (-1 * x3) < 19; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-010.cvc b/test/regress/regress1/arith/arith-int-010.cvc new file mode 100644 index 000000000..4ac85a984 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-010.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (19 * x0) + (-2 * x1) + (-29 * x2) + (-24 * x3) = 3 ; +ASSERT (3 * x0) + (11 * x1) + (-14 * x2) + (6 * x3) = 4 ; +ASSERT (-1 * x0) + (-22 * x1) + (4 * x2) + (5 * x3) = -22; +ASSERT (8 * x0) + (-8 * x1) + (18 * x2) + (-14 * x3) < -20 ; +ASSERT (22 * x0) + (27 * x1) + (6 * x2) + (-3 * x3) <= -11 ; +ASSERT (-23 * x0) + (-29 * x1) + (-27 * x2) + (13 * x3) <= 3 ; +ASSERT (8 * x0) + (0 * x1) + (28 * x2) + (0 * x3) >= -29 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-011.cvc b/test/regress/regress1/arith/arith-int-011.cvc new file mode 100644 index 000000000..bd2fa2a0d --- /dev/null +++ b/test/regress/regress1/arith/arith-int-011.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (13 * x0) + (-1 * x1) + (11 * x2) + (10 * x3) = 9 ; +ASSERT (-7 * x0) + (3 * x1) + (-22 * x2) + (16 * x3) >= 9; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-012.cvc b/test/regress/regress1/arith/arith-int-012.cvc new file mode 100644 index 000000000..11b0dab27 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-012.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (18 * x0) + (32 * x1) + (-11 * x2) + (18 * x3) < -25 ; +ASSERT (-31 * x0) + (16 * x1) + (24 * x2) + (9 * x3) >= -24; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-013.cvc b/test/regress/regress1/arith/arith-int-013.cvc new file mode 100644 index 000000000..329251cae --- /dev/null +++ b/test/regress/regress1/arith/arith-int-013.cvc @@ -0,0 +1,5 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-22 * x0) + (-14 * x1) + (4 * x2) + (-12 * x3) > 25 ; +ASSERT (14 * x0) + (11 * x1) + (32 * x2) + (-8 * x3) >= 2; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-016.cvc b/test/regress/regress1/arith/arith-int-016.cvc new file mode 100644 index 000000000..6774dd2d1 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-016.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (-4 * x1) + (-20 * x2) + (-26 * x3) = 2 ; +ASSERT (13 * x0) + (13 * x1) + (-14 * x2) + (26 * x3) = -8 ; +ASSERT (-13 * x0) + (1 * x1) + (16 * x2) + (4 * x3) = -22 ; +ASSERT (17 * x0) + (7 * x1) + (32 * x2) + (19 * x3) = 16 ; +ASSERT (11 * x0) + (-8 * x1) + (-10 * x2) + (-10 * x3) <= -1 ; +ASSERT (-25 * x0) + (-18 * x1) + (-10 * x2) + (-19 * x3) <= 32 ; +ASSERT (0 * x0) + (-14 * x1) + (30 * x2) + (-5 * x3) > -13 ; +ASSERT (2 * x0) + (-17 * x1) + (-13 * x2) + (8 * x3) > 1 ; +ASSERT (-4 * x0) + (-1 * x1) + (29 * x2) + (-9 * x3) > -8 ; +ASSERT (-32 * x0) + (26 * x1) + (5 * x2) + (6 * x3) <= -1 ; +ASSERT (-26 * x0) + (3 * x1) + (22 * x2) + (27 * x3) > -2 ; +ASSERT (13 * x0) + (3 * x1) + (1 * x2) + (9 * x3) < 24 ; +ASSERT (-10 * x0) + (22 * x1) + (5 * x2) + (-5 * x3) >= -21 ; +ASSERT (-20 * x0) + (-28 * x1) + (-11 * x2) + (6 * x3) >= -17 ; +ASSERT (14 * x0) + (16 * x1) + (-15 * x2) + (17 * x3) < 27 ; +ASSERT (-23 * x0) + (-4 * x1) + (-19 * x2) + (-23 * x3) < 20 ; +ASSERT (-8 * x0) + (-5 * x1) + (-17 * x2) + (32 * x3) <= 20; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-017.cvc b/test/regress/regress1/arith/arith-int-017.cvc new file mode 100644 index 000000000..e9a06125a --- /dev/null +++ b/test/regress/regress1/arith/arith-int-017.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (23 * x0) + (-4 * x1) + (-26 * x2) + (-1 * x3) = 10 ; +ASSERT (15 * x0) + (31 * x1) + (31 * x2) + (31 * x3) = 13 ; +ASSERT (19 * x0) + (-15 * x1) + (25 * x2) + (30 * x3) = 23 ; +ASSERT (10 * x0) + (-17 * x1) + (15 * x2) + (13 * x3) < 22 ; +ASSERT (-7 * x0) + (22 * x1) + (8 * x2) + (24 * x3) < 14 ; +ASSERT (24 * x0) + (-12 * x1) + (0 * x2) + (-25 * x3) <= -19 ; +ASSERT (-27 * x0) + (17 * x1) + (-20 * x2) + (-25 * x3) >= 11 ; +ASSERT (3 * x0) + (-12 * x1) + (-18 * x2) + (15 * x3) > -27 ; +ASSERT (-19 * x0) + (24 * x1) + (9 * x2) + (4 * x3) <= 16 ; +ASSERT (28 * x0) + (-20 * x1) + (-21 * x2) + (4 * x3) > -13 ; +ASSERT (-21 * x0) + (-23 * x1) + (-31 * x2) + (-6 * x3) < 6 ; +ASSERT (-30 * x0) + (8 * x1) + (-22 * x2) + (8 * x3) > 14 ; +ASSERT (-1 * x0) + (17 * x1) + (-22 * x2) + (-4 * x3) >= 4 ; +ASSERT (2 * x0) + (-4 * x1) + (10 * x2) + (30 * x3) < -15 ; +ASSERT (29 * x0) + (27 * x1) + (23 * x2) + (-4 * x3) < 21 ; +ASSERT (-28 * x0) + (0 * x1) + (19 * x2) + (7 * x3) <= -18 ; +ASSERT (-20 * x0) + (-7 * x1) + (26 * x2) + (-17 * x3) < 23; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-018.cvc b/test/regress/regress1/arith/arith-int-018.cvc new file mode 100644 index 000000000..4cb97b77e --- /dev/null +++ b/test/regress/regress1/arith/arith-int-018.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-11 * x0) + (-26 * x1) + (9 * x2) + (32 * x3) = -11 ; +ASSERT (-5 * x0) + (-11 * x1) + (-10 * x2) + (-31 * x3) = -23 ; +ASSERT (-12 * x0) + (9 * x1) + (-22 * x2) + (11 * x3) = 11 ; +ASSERT (-27 * x0) + (8 * x1) + (-28 * x2) + (-7 * x3) = 23 ; +ASSERT (19 * x0) + (4 * x1) + (5 * x2) + (-10 * x3) >= 2 ; +ASSERT (-6 * x0) + (-20 * x1) + (30 * x2) + (20 * x3) >= 12 ; +ASSERT (19 * x0) + (26 * x1) + (-21 * x2) + (18 * x3) <= -21 ; +ASSERT (8 * x0) + (-29 * x1) + (7 * x2) + (20 * x3) >= 29 ; +ASSERT (-28 * x0) + (6 * x1) + (11 * x2) + (0 * x3) >= -4 ; +ASSERT (-20 * x0) + (-30 * x1) + (17 * x2) + (25 * x3) >= 4 ; +ASSERT (-15 * x0) + (9 * x1) + (9 * x2) + (26 * x3) > 11 ; +ASSERT (-30 * x0) + (-20 * x1) + (-20 * x2) + (14 * x3) <= -27 ; +ASSERT (-22 * x0) + (-11 * x1) + (-6 * x2) + (18 * x3) > -13 ; +ASSERT (-22 * x0) + (-25 * x1) + (22 * x2) + (-24 * x3) <= 1 ; +ASSERT (-24 * x0) + (22 * x1) + (-28 * x2) + (-14 * x3) >= 18 ; +ASSERT (17 * x0) + (31 * x1) + (-13 * x2) + (-23 * x3) < -5 ; +ASSERT (-12 * x0) + (-28 * x1) + (19 * x2) + (-21 * x3) < -27; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-019.cvc b/test/regress/regress1/arith/arith-int-019.cvc new file mode 100644 index 000000000..cf9ae2d70 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-019.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (25 * x0) + (6 * x1) + (-30 * x2) + (29 * x3) = -5 ; +ASSERT (14 * x0) + (16 * x1) + (24 * x2) + (-7 * x3) <= 31 ; +ASSERT (1 * x0) + (20 * x1) + (14 * x2) + (5 * x3) >= 3 ; +ASSERT (-5 * x0) + (24 * x1) + (-21 * x2) + (-13 * x3) >= -12 ; +ASSERT (9 * x0) + (-16 * x1) + (23 * x2) + (-11 * x3) > -5 ; +ASSERT (-24 * x0) + (26 * x1) + (19 * x2) + (29 * x3) > -27 ; +ASSERT (-30 * x0) + (31 * x1) + (27 * x2) + (-26 * x3) < 23 ; +ASSERT (14 * x0) + (1 * x1) + (0 * x2) + (29 * x3) > 21 ; +ASSERT (-32 * x0) + (-5 * x1) + (27 * x2) + (31 * x3) <= 23 ; +ASSERT (30 * x0) + (10 * x1) + (30 * x2) + (29 * x3) < -28 ; +ASSERT (7 * x0) + (-4 * x1) + (-25 * x2) + (0 * x3) > -28 ; +ASSERT (3 * x0) + (-19 * x1) + (11 * x2) + (-21 * x3) <= 10 ; +ASSERT (-31 * x0) + (21 * x1) + (24 * x2) + (-17 * x3) >= 21 ; +ASSERT (-20 * x0) + (19 * x1) + (6 * x2) + (5 * x3) >= -27 ; +ASSERT (-8 * x0) + (-27 * x1) + (0 * x2) + (13 * x3) >= 12 ; +ASSERT (-21 * x0) + (7 * x1) + (-26 * x2) + (19 * x3) < -10 ; +ASSERT (32 * x0) + (-26 * x1) + (-24 * x2) + (14 * x3) < 13; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-020.cvc b/test/regress/regress1/arith/arith-int-020.cvc new file mode 100644 index 000000000..07a827465 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-020.cvc @@ -0,0 +1,20 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-32 * x0) + (31 * x1) + (-32 * x2) + (-21 * x3) = 5 ; +ASSERT (32 * x0) + (5 * x1) + (23 * x2) + (-16 * x3) = 8 ; +ASSERT (-17 * x0) + (-17 * x1) + (-22 * x2) + (30 * x3) = -5 ; +ASSERT (30 * x0) + (18 * x1) + (26 * x2) + (6 * x3) = -8 ; +ASSERT (17 * x0) + (-4 * x1) + (-16 * x2) + (-22 * x3) = 11; +ASSERT (0 * x0) + (-26 * x1) + (-15 * x2) + (12 * x3) > 7 ; +ASSERT (-30 * x0) + (4 * x1) + (-1 * x2) + (27 * x3) > 11 ; +ASSERT (23 * x0) + (12 * x1) + (11 * x2) + (-2 * x3) <= -10 ; +ASSERT (-26 * x0) + (-8 * x1) + (7 * x2) + (-18 * x3) > 1 ; +ASSERT (3 * x0) + (0 * x1) + (5 * x2) + (24 * x3) > 2 ; +ASSERT (-13 * x0) + (15 * x1) + (2 * x2) + (2 * x3) <= 17 ; +ASSERT (-24 * x0) + (21 * x1) + (-21 * x2) + (-13 * x3) >= -30 ; +ASSERT (7 * x0) + (-11 * x1) + (2 * x2) + (21 * x3) >= -24 ; +ASSERT (-15 * x0) + (-1 * x1) + (6 * x2) + (-10 * x3) <= -25 ; +ASSERT (-21 * x0) + (8 * x1) + (3 * x2) + (-5 * x3) <= 22 ; +ASSERT (-18 * x0) + (-16 * x1) + (21 * x2) + (20 * x3) >= 9 ; +ASSERT (-17 * x0) + (-10 * x1) + (-20 * x2) + (16 * x3) >= 3 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-022.cvc b/test/regress/regress1/arith/arith-int-022.cvc new file mode 100644 index 000000000..584348da4 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-022.cvc @@ -0,0 +1,4 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-24 * x0) + (25 * x1) + (-28 * x2) + (31 * x3) > 18; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-024.cvc b/test/regress/regress1/arith/arith-int-024.cvc new file mode 100644 index 000000000..f57136dd1 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-024.cvc @@ -0,0 +1,4 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (4 * x0) + (8 * x1) + (27 * x2) + (-12 * x3) = -5; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-026.cvc b/test/regress/regress1/arith/arith-int-026.cvc new file mode 100644 index 000000000..9e69aa2d1 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-026.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (25 * x1) + (1 * x2) + (-11 * x3) = 19 ; +ASSERT (-10 * x0) + (-27 * x1) + (6 * x2) + (6 * x3) = 28 ; +ASSERT (0 * x0) + (-30 * x1) + (-31 * x2) + (12 * x3) = -21 ; +ASSERT (29 * x0) + (-6 * x1) + (-12 * x2) + (22 * x3) = -13; +ASSERT (-7 * x0) + (23 * x1) + (-1 * x2) + (-14 * x3) > -6 ; +ASSERT (-27 * x0) + (-31 * x1) + (25 * x2) + (-23 * x3) <= 12 ; +ASSERT (-19 * x0) + (6 * x1) + (0 * x2) + (-28 * x3) > -1 ; +ASSERT (-12 * x0) + (19 * x1) + (2 * x2) + (-4 * x3) <= 12 ; +ASSERT (10 * x0) + (-26 * x1) + (7 * x2) + (-6 * x3) < 12 ; +ASSERT (25 * x0) + (-18 * x1) + (-30 * x2) + (-9 * x3) < -2 ; +ASSERT (-9 * x0) + (-13 * x1) + (-9 * x2) + (-28 * x3) > 18 ; +ASSERT (-12 * x0) + (-28 * x1) + (-21 * x2) + (32 * x3) > 18 ; +ASSERT (-23 * x0) + (-26 * x1) + (-21 * x2) + (-24 * x3) <= 3 ; +ASSERT (-15 * x0) + (13 * x1) + (-4 * x2) + (-1 * x3) <= 0 ; +ASSERT (11 * x0) + (-30 * x1) + (3 * x2) + (-6 * x3) >= 3 ; +ASSERT (28 * x0) + (0 * x1) + (0 * x2) + (-22 * x3) >= 9 ; +ASSERT (-18 * x0) + (15 * x1) + (-27 * x2) + (31 * x3) < 5 ; +ASSERT (10 * x0) + (30 * x1) + (-28 * x2) + (27 * x3) <= -1 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-027.cvc b/test/regress/regress1/arith/arith-int-027.cvc new file mode 100644 index 000000000..b45622fea --- /dev/null +++ b/test/regress/regress1/arith/arith-int-027.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (17 * x0) + (29 * x1) + (-11 * x2) + (24 * x3) = 13 ; +ASSERT (16 * x0) + (-20 * x1) + (-5 * x2) + (12 * x3) = 13 ; +ASSERT (-12 * x0) + (-3 * x1) + (-19 * x2) + (4 * x3) = -21 ; +ASSERT (-3 * x0) + (10 * x1) + (-6 * x2) + (-31 * x3) = 21 ; +ASSERT (10 * x0) + (-14 * x1) + (-12 * x2) + (8 * x3) = 5 ; +ASSERT (-4 * x0) + (15 * x1) + (29 * x2) + (2 * x3) = -32 ; +ASSERT (-14 * x0) + (-12 * x1) + (16 * x2) + (-14 * x3) = -8 ; +ASSERT (-31 * x0) + (14 * x1) + (30 * x2) + (-19 * x3) < -20 ; +ASSERT (-5 * x0) + (9 * x1) + (11 * x2) + (-32 * x3) < 3 ; +ASSERT (27 * x0) + (-6 * x1) + (0 * x2) + (30 * x3) <= -20 ; +ASSERT (-15 * x0) + (-13 * x1) + (-21 * x2) + (-5 * x3) > -8 ; +ASSERT (19 * x0) + (31 * x1) + (-16 * x2) + (-8 * x3) > -15 ; +ASSERT (9 * x0) + (-9 * x1) + (-4 * x2) + (-16 * x3) < 21 ; +ASSERT (24 * x0) + (4 * x1) + (28 * x2) + (-14 * x3) >= -1 ; +ASSERT (5 * x0) + (23 * x1) + (-22 * x2) + (-28 * x3) >= -21 ; +ASSERT (-31 * x0) + (14 * x1) + (14 * x2) + (-9 * x3) > -32 ; +ASSERT (25 * x0) + (-18 * x1) + (21 * x2) + (-17 * x3) < -20 ; +ASSERT (1 * x0) + (-29 * x1) + (11 * x2) + (-24 * x3) >= -20; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-028.cvc b/test/regress/regress1/arith/arith-int-028.cvc new file mode 100644 index 000000000..61fee4203 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-028.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-31 * x0) + (-5 * x1) + (-28 * x2) + (16 * x3) = 10 ; +ASSERT (3 * x0) + (-20 * x1) + (-11 * x2) + (-2 * x3) = 25 ; +ASSERT (31 * x0) + (28 * x1) + (-20 * x2) + (15 * x3) = -30; +ASSERT (15 * x0) + (-16 * x1) + (29 * x2) + (-2 * x3) >= -6 ; +ASSERT (-29 * x0) + (-17 * x1) + (-7 * x2) + (11 * x3) < 26 ; +ASSERT (-4 * x0) + (14 * x1) + (-29 * x2) + (-7 * x3) >= 28 ; +ASSERT (-29 * x0) + (-25 * x1) + (9 * x2) + (-17 * x3) <= -25 ; +ASSERT (10 * x0) + (-25 * x1) + (28 * x2) + (8 * x3) > 6 ; +ASSERT (10 * x0) + (17 * x1) + (-1 * x2) + (21 * x3) > 24 ; +ASSERT (-19 * x0) + (-29 * x1) + (-26 * x2) + (-7 * x3) <= -11 ; +ASSERT (30 * x0) + (-7 * x1) + (-8 * x2) + (6 * x3) >= -32 ; +ASSERT (-3 * x0) + (24 * x1) + (30 * x2) + (-30 * x3) >= 19 ; +ASSERT (-9 * x0) + (5 * x1) + (17 * x2) + (-24 * x3) < -22 ; +ASSERT (11 * x0) + (-16 * x1) + (-1 * x2) + (26 * x3) >= 1 ; +ASSERT (-13 * x0) + (5 * x1) + (19 * x2) + (4 * x3) >= 27 ; +ASSERT (23 * x0) + (4 * x1) + (30 * x2) + (-28 * x3) > 13 ; +ASSERT (-8 * x0) + (-24 * x1) + (0 * x2) + (22 * x3) < -6 ; +ASSERT (-1 * x0) + (1 * x1) + (-30 * x2) + (12 * x3) >= -26 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-029.cvc b/test/regress/regress1/arith/arith-int-029.cvc new file mode 100644 index 000000000..ee49bbb68 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-029.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-29 * x0) + (-17 * x1) + (11 * x2) + (1 * x3) = -15 ; +ASSERT (-13 * x0) + (1 * x1) + (-6 * x2) + (-15 * x3) = 32 ; +ASSERT (-19 * x0) + (29 * x1) + (27 * x2) + (-8 * x3) = -4 ; +ASSERT (-28 * x0) + (-15 * x1) + (-20 * x2) + (-1 * x3) = -2 ; +ASSERT (-2 * x0) + (2 * x1) + (3 * x2) + (-4 * x3) = 16 ; +ASSERT (31 * x0) + (22 * x1) + (15 * x2) + (28 * x3) = -19 ; +ASSERT (-32 * x0) + (2 * x1) + (-8 * x2) + (6 * x3) <= -21 ; +ASSERT (-10 * x0) + (23 * x1) + (-9 * x2) + (-26 * x3) < -7 ; +ASSERT (-11 * x0) + (-13 * x1) + (-17 * x2) + (-19 * x3) >= -11 ; +ASSERT (20 * x0) + (11 * x1) + (-11 * x2) + (-7 * x3) <= 14 ; +ASSERT (17 * x0) + (0 * x1) + (-27 * x2) + (-32 * x3) > -1 ; +ASSERT (17 * x0) + (-7 * x1) + (18 * x2) + (-29 * x3) > -19 ; +ASSERT (12 * x0) + (-14 * x1) + (27 * x2) + (5 * x3) <= 23 ; +ASSERT (-2 * x0) + (-6 * x1) + (-6 * x2) + (19 * x3) < -5 ; +ASSERT (-3 * x0) + (-10 * x1) + (-30 * x2) + (18 * x3) >= -27 ; +ASSERT (-18 * x0) + (-25 * x1) + (3 * x2) + (2 * x3) < -25 ; +ASSERT (-19 * x0) + (16 * x1) + (-11 * x2) + (-26 * x3) >= -24 ; +ASSERT (-2 * x0) + (21 * x1) + (25 * x2) + (28 * x3) > 10; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-030.cvc b/test/regress/regress1/arith/arith-int-030.cvc new file mode 100644 index 000000000..70b6a3785 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-030.cvc @@ -0,0 +1,21 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (26 * x1) + (-11 * x2) + (17 * x3) = 17 ; +ASSERT (-15 * x0) + (2 * x1) + (-9 * x2) + (17 * x3) = -11 ; +ASSERT (8 * x0) + (-24 * x1) + (20 * x2) + (23 * x3) = -23 ; +ASSERT (-2 * x0) + (26 * x1) + (4 * x2) + (31 * x3) < 31 ; +ASSERT (23 * x0) + (14 * x1) + (-29 * x2) + (-11 * x3) > 14 ; +ASSERT (-19 * x0) + (-32 * x1) + (11 * x2) + (31 * x3) < -4 ; +ASSERT (3 * x0) + (13 * x1) + (-19 * x2) + (26 * x3) >= -20 ; +ASSERT (-6 * x0) + (4 * x1) + (-17 * x2) + (-31 * x3) <= 32 ; +ASSERT (-13 * x0) + (32 * x1) + (-18 * x2) + (7 * x3) < -27 ; +ASSERT (-19 * x0) + (6 * x1) + (-28 * x2) + (-15 * x3) >= 30 ; +ASSERT (30 * x0) + (-24 * x1) + (-10 * x2) + (-4 * x3) >= -9 ; +ASSERT (-4 * x0) + (4 * x1) + (-27 * x2) + (-17 * x3) < 12 ; +ASSERT (-21 * x0) + (13 * x1) + (31 * x2) + (4 * x3) >= -16 ; +ASSERT (-11 * x0) + (30 * x1) + (-20 * x2) + (21 * x3) <= 9 ; +ASSERT (-12 * x0) + (23 * x1) + (2 * x2) + (12 * x3) <= 18 ; +ASSERT (30 * x0) + (8 * x1) + (4 * x2) + (-5 * x3) <= -24 ; +ASSERT (12 * x0) + (22 * x1) + (9 * x2) + (30 * x3) >= -3 ; +ASSERT (10 * x0) + (15 * x1) + (25 * x2) + (-5 * x3) <= 4; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-031.cvc b/test/regress/regress1/arith/arith-int-031.cvc new file mode 100644 index 000000000..86242f7aa --- /dev/null +++ b/test/regress/regress1/arith/arith-int-031.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-21 * x0) + (-24 * x1) + (-31 * x2) + (12 * x3) = -10 ; +ASSERT (-4 * x0) + (22 * x1) + (9 * x2) + (17 * x3) > -20 ; +ASSERT (0 * x0) + (22 * x1) + (-11 * x2) + (-22 * x3) <= 26 ; +ASSERT (17 * x0) + (-11 * x1) + (32 * x2) + (8 * x3) < 20 ; +ASSERT (-30 * x0) + (24 * x1) + (-30 * x2) + (-12 * x3) >= 19 ; +ASSERT (-27 * x0) + (5 * x1) + (31 * x2) + (-12 * x3) <= -24 ; +ASSERT (-12 * x0) + (-23 * x1) + (-27 * x2) + (29 * x3) >= 13 ; +ASSERT (23 * x0) + (-21 * x1) + (24 * x2) + (-17 * x3) >= -20 ; +ASSERT (-30 * x0) + (-27 * x1) + (-21 * x2) + (-11 * x3) < -24 ; +ASSERT (31 * x0) + (-14 * x1) + (-3 * x2) + (-9 * x3) >= 13 ; +ASSERT (8 * x0) + (-2 * x1) + (-13 * x2) + (23 * x3) < 31 ; +ASSERT (-1 * x0) + (9 * x1) + (-29 * x2) + (17 * x3) >= -7 ; +ASSERT (11 * x0) + (-8 * x1) + (-29 * x2) + (-25 * x3) >= -5 ; +ASSERT (19 * x0) + (-32 * x1) + (27 * x2) + (17 * x3) > 17 ; +ASSERT (23 * x0) + (-1 * x1) + (-9 * x2) + (-12 * x3) < -25 ; +ASSERT (16 * x0) + (-22 * x1) + (3 * x2) + (30 * x3) >= 11; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-032.cvc b/test/regress/regress1/arith/arith-int-032.cvc new file mode 100644 index 000000000..1ee4c9844 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-032.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (4 * x0) + (-29 * x1) + (-9 * x2) + (9 * x3) = 8 ; +ASSERT (-26 * x0) + (-26 * x1) + (26 * x2) + (-18 * x3) = -20 ; +ASSERT (-15 * x0) + (-4 * x1) + (-28 * x2) + (-25 * x3) = 13 ; +ASSERT (17 * x0) + (-29 * x1) + (19 * x2) + (-32 * x3) = 26 ; +ASSERT (20 * x0) + (-29 * x1) + (-32 * x2) + (28 * x3) = -12 ; +ASSERT (17 * x0) + (18 * x1) + (-18 * x2) + (28 * x3) <= 21 ; +ASSERT (-28 * x0) + (-17 * x1) + (-15 * x2) + (30 * x3) > -19 ; +ASSERT (-6 * x0) + (-25 * x1) + (-22 * x2) + (-13 * x3) < -8 ; +ASSERT (12 * x0) + (8 * x1) + (15 * x2) + (-7 * x3) >= 12 ; +ASSERT (14 * x0) + (6 * x1) + (3 * x2) + (25 * x3) > 3 ; +ASSERT (31 * x0) + (5 * x1) + (26 * x2) + (-1 * x3) < -13 ; +ASSERT (31 * x0) + (-27 * x1) + (15 * x2) + (-16 * x3) >= 11 ; +ASSERT (20 * x0) + (-20 * x1) + (25 * x2) + (18 * x3) > 18 ; +ASSERT (-2 * x0) + (-30 * x1) + (25 * x2) + (-9 * x3) < -9 ; +ASSERT (29 * x0) + (-22 * x1) + (-18 * x2) + (-25 * x3) < -2 ; +ASSERT (-12 * x0) + (9 * x1) + (17 * x2) + (-16 * x3) > 3; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-033.cvc b/test/regress/regress1/arith/arith-int-033.cvc new file mode 100644 index 000000000..599ba4e9a --- /dev/null +++ b/test/regress/regress1/arith/arith-int-033.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-14 * x0) + (16 * x1) + (-16 * x2) + (0 * x3) = -8 ; +ASSERT (3 * x0) + (-20 * x1) + (-12 * x2) + (-3 * x3) = -7 ; +ASSERT (-28 * x0) + (31 * x1) + (32 * x2) + (-11 * x3) = 0 ; +ASSERT (-20 * x0) + (-11 * x1) + (-27 * x2) + (-6 * x3) = -6 ; +ASSERT (-7 * x0) + (-7 * x1) + (17 * x2) + (-25 * x3) <= -15 ; +ASSERT (8 * x0) + (28 * x1) + (8 * x2) + (7 * x3) > -28 ; +ASSERT (25 * x0) + (7 * x1) + (-17 * x2) + (-28 * x3) > 5 ; +ASSERT (-19 * x0) + (0 * x1) + (-20 * x2) + (0 * x3) <= 20 ; +ASSERT (6 * x0) + (2 * x1) + (29 * x2) + (-19 * x3) <= -3 ; +ASSERT (-9 * x0) + (-1 * x1) + (-18 * x2) + (32 * x3) > 11 ; +ASSERT (2 * x0) + (21 * x1) + (0 * x2) + (19 * x3) >= 13 ; +ASSERT (-26 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) < -24 ; +ASSERT (-23 * x0) + (22 * x1) + (12 * x2) + (19 * x3) < -27 ; +ASSERT (-25 * x0) + (-31 * x1) + (28 * x2) + (14 * x3) < 14 ; +ASSERT (-29 * x0) + (1 * x1) + (26 * x2) + (-27 * x3) < -14 ; +ASSERT (23 * x0) + (26 * x1) + (-5 * x2) + (6 * x3) <= -19; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-034.cvc b/test/regress/regress1/arith/arith-int-034.cvc new file mode 100644 index 000000000..ec615a785 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-034.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (-5 * x1) + (30 * x2) + (-24 * x3) = 12 ; +ASSERT (24 * x0) + (27 * x1) + (18 * x2) + (-5 * x3) = -16 ; +ASSERT (14 * x0) + (11 * x1) + (17 * x2) + (12 * x3) = -5 ; +ASSERT (-29 * x0) + (-29 * x1) + (-16 * x2) + (14 * x3) = 10 ; +ASSERT (30 * x0) + (13 * x1) + (10 * x2) + (24 * x3) = 3 ; +ASSERT (-20 * x0) + (29 * x1) + (28 * x2) + (27 * x3) < -21 ; +ASSERT (-31 * x0) + (17 * x1) + (14 * x2) + (-14 * x3) <= 14 ; +ASSERT (-23 * x0) + (19 * x1) + (28 * x2) + (-2 * x3) > -28 ; +ASSERT (-23 * x0) + (23 * x1) + (19 * x2) + (25 * x3) > 13 ; +ASSERT (-32 * x0) + (8 * x1) + (-24 * x2) + (10 * x3) >= -5 ; +ASSERT (-30 * x0) + (1 * x1) + (-22 * x2) + (12 * x3) >= -30 ; +ASSERT (8 * x0) + (28 * x1) + (17 * x2) + (-7 * x3) < -20 ; +ASSERT (-28 * x0) + (-8 * x1) + (27 * x2) + (25 * x3) >= 7 ; +ASSERT (-15 * x0) + (26 * x1) + (9 * x2) + (15 * x3) > -12 ; +ASSERT (-3 * x0) + (15 * x1) + (-6 * x2) + (-31 * x3) < -24 ; +ASSERT (-26 * x0) + (22 * x1) + (16 * x2) + (30 * x3) <= -2; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-035.cvc b/test/regress/regress1/arith/arith-int-035.cvc new file mode 100644 index 000000000..e7dee2484 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-035.cvc @@ -0,0 +1,19 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-3 * x0) + (2 * x1) + (17 * x2) + (-4 * x3) = -17 ; +ASSERT (5 * x0) + (-4 * x1) + (22 * x2) + (14 * x3) = -15 ; +ASSERT (8 * x0) + (23 * x1) + (26 * x2) + (-1 * x3) >= -6 ; +ASSERT (-7 * x0) + (4 * x1) + (9 * x2) + (-30 * x3) > -26 ; +ASSERT (-14 * x0) + (-31 * x1) + (-18 * x2) + (-5 * x3) <= 6 ; +ASSERT (15 * x0) + (26 * x1) + (3 * x2) + (-24 * x3) >= 6 ; +ASSERT (13 * x0) + (0 * x1) + (25 * x2) + (-27 * x3) <= -13 ; +ASSERT (11 * x0) + (20 * x1) + (-28 * x2) + (8 * x3) < 0 ; +ASSERT (-10 * x0) + (13 * x1) + (20 * x2) + (19 * x3) >= 29 ; +ASSERT (12 * x0) + (-9 * x1) + (-16 * x2) + (26 * x3) >= -11 ; +ASSERT (-2 * x0) + (32 * x1) + (-6 * x2) + (21 * x3) > -31 ; +ASSERT (-1 * x0) + (-22 * x1) + (-22 * x2) + (-5 * x3) > 29 ; +ASSERT (-8 * x0) + (19 * x1) + (18 * x2) + (32 * x3) >= 12 ; +ASSERT (26 * x0) + (16 * x1) + (-25 * x2) + (29 * x3) < 29 ; +ASSERT (1 * x0) + (-18 * x1) + (11 * x2) + (-10 * x3) > 10 ; +ASSERT (-21 * x0) + (5 * x1) + (-2 * x2) + (-28 * x3) <= -5; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-036.cvc b/test/regress/regress1/arith/arith-int-036.cvc new file mode 100644 index 000000000..9594f9586 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-036.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-9 * x0) + (-21 * x1) + (-25 * x2) + (-1 * x3) = -11 ; +ASSERT (31 * x0) + (-18 * x1) + (5 * x2) + (-11 * x3) = 10 ; +ASSERT (15 * x0) + (5 * x1) + (5 * x2) + (19 * x3) = -29 ; +ASSERT (-9 * x0) + (-23 * x1) + (7 * x2) + (-21 * x3) = 28 ; +ASSERT (-24 * x0) + (-22 * x1) + (30 * x2) + (-31 * x3) = -24 ; +ASSERT (-29 * x0) + (-21 * x1) + (26 * x2) + (-13 * x3) < -12 ; +ASSERT (31 * x0) + (6 * x1) + (-23 * x2) + (30 * x3) < -3 ; +ASSERT (21 * x0) + (-7 * x1) + (-4 * x2) + (-25 * x3) <= -17 ; +ASSERT (4 * x0) + (24 * x1) + (21 * x2) + (8 * x3) <= 19 ; +ASSERT (19 * x0) + (30 * x1) + (14 * x2) + (-23 * x3) > 21 ; +ASSERT (30 * x0) + (3 * x1) + (-28 * x2) + (25 * x3) <= -27 ; +ASSERT (0 * x0) + (-17 * x1) + (-9 * x2) + (-8 * x3) <= 31 ; +ASSERT (-6 * x0) + (-23 * x1) + (21 * x2) + (18 * x3) >= 31; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-037.cvc b/test/regress/regress1/arith/arith-int-037.cvc new file mode 100644 index 000000000..4d4422d3f --- /dev/null +++ b/test/regress/regress1/arith/arith-int-037.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (12 * x0) + (14 * x1) + (-22 * x2) + (-6 * x3) = 29 ; +ASSERT (-9 * x0) + (14 * x1) + (-23 * x2) + (-31 * x3) = 4 ; +ASSERT (-10 * x0) + (7 * x1) + (-23 * x2) + (18 * x3) <= -16 ; +ASSERT (-12 * x0) + (7 * x1) + (-16 * x2) + (16 * x3) > -31 ; +ASSERT (10 * x0) + (11 * x1) + (-17 * x2) + (19 * x3) <= 9 ; +ASSERT (-1 * x0) + (-8 * x1) + (-31 * x2) + (16 * x3) > 20 ; +ASSERT (-9 * x0) + (18 * x1) + (9 * x2) + (-14 * x3) <= -8 ; +ASSERT (-9 * x0) + (27 * x1) + (-22 * x2) + (-16 * x3) > 27 ; +ASSERT (-24 * x0) + (-25 * x1) + (-28 * x2) + (29 * x3) <= -9 ; +ASSERT (4 * x0) + (13 * x1) + (27 * x2) + (-5 * x3) >= -22 ; +ASSERT (-20 * x0) + (-14 * x1) + (21 * x2) + (-28 * x3) <= 17 ; +ASSERT (18 * x0) + (-32 * x1) + (-23 * x2) + (-9 * x3) <= -21 ; +ASSERT (19 * x0) + (-9 * x1) + (18 * x2) + (-9 * x3) <= -19; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-038.cvc b/test/regress/regress1/arith/arith-int-038.cvc new file mode 100644 index 000000000..476133b24 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-038.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-24 * x0) + (25 * x1) + (28 * x2) + (-31 * x3) = -1 ; +ASSERT (29 * x0) + (17 * x1) + (-2 * x2) + (-6 * x3) <= 4 ; +ASSERT (-16 * x0) + (-4 * x1) + (-2 * x2) + (-1 * x3) >= -28 ; +ASSERT (4 * x0) + (-26 * x1) + (2 * x2) + (-8 * x3) > 7 ; +ASSERT (-17 * x0) + (-6 * x1) + (11 * x2) + (-9 * x3) > -27 ; +ASSERT (-25 * x0) + (13 * x1) + (-29 * x2) + (15 * x3) > 2 ; +ASSERT (32 * x0) + (-10 * x1) + (15 * x2) + (-25 * x3) < -25 ; +ASSERT (-16 * x0) + (-26 * x1) + (16 * x2) + (3 * x3) > -26 ; +ASSERT (-14 * x0) + (13 * x1) + (4 * x2) + (-24 * x3) >= -14 ; +ASSERT (-5 * x0) + (-21 * x1) + (-7 * x2) + (10 * x3) < 0 ; +ASSERT (0 * x0) + (25 * x1) + (31 * x2) + (30 * x3) <= -25 ; +ASSERT (-1 * x0) + (2 * x1) + (26 * x2) + (4 * x3) <= 4 ; +ASSERT (14 * x0) + (23 * x1) + (18 * x2) + (-18 * x3) > 19; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-039.cvc b/test/regress/regress1/arith/arith-int-039.cvc new file mode 100644 index 000000000..9e9235ae8 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-039.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (21 * x1) + (-18 * x2) + (21 * x3) = 30 ; +ASSERT (-31 * x0) + (22 * x1) + (-20 * x2) + (18 * x3) = -32 ; +ASSERT (12 * x0) + (18 * x1) + (29 * x2) + (17 * x3) = 0 ; +ASSERT (-8 * x0) + (-10 * x1) + (-27 * x2) + (30 * x3) = 32 ; +ASSERT (-21 * x0) + (-2 * x1) + (20 * x2) + (-7 * x3) <= -27 ; +ASSERT (-7 * x0) + (-22 * x1) + (8 * x2) + (20 * x3) > -20 ; +ASSERT (-10 * x0) + (1 * x1) + (21 * x2) + (-6 * x3) > 10 ; +ASSERT (-21 * x0) + (-24 * x1) + (-15 * x2) + (4 * x3) <= 11 ; +ASSERT (-32 * x0) + (10 * x1) + (-21 * x2) + (-17 * x3) <= 5 ; +ASSERT (7 * x0) + (-19 * x1) + (28 * x2) + (27 * x3) <= 14 ; +ASSERT (-32 * x0) + (5 * x1) + (26 * x2) + (-23 * x3) < -23 ; +ASSERT (-28 * x0) + (5 * x1) + (22 * x2) + (25 * x3) < 6 ; +ASSERT (4 * x0) + (17 * x1) + (11 * x2) + (26 * x3) >= 20; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-040.cvc b/test/regress/regress1/arith/arith-int-040.cvc new file mode 100644 index 000000000..68502349f --- /dev/null +++ b/test/regress/regress1/arith/arith-int-040.cvc @@ -0,0 +1,16 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-1 * x0) + (-24 * x1) + (3 * x2) + (-8 * x3) > -5 ; +ASSERT (29 * x0) + (17 * x1) + (-26 * x2) + (20 * x3) > 11 ; +ASSERT (18 * x0) + (15 * x1) + (-27 * x2) + (8 * x3) > -11 ; +ASSERT (-14 * x0) + (4 * x1) + (27 * x2) + (-9 * x3) < -13 ; +ASSERT (24 * x0) + (11 * x1) + (17 * x2) + (-15 * x3) > 5 ; +ASSERT (-28 * x0) + (-1 * x1) + (10 * x2) + (-12 * x3) > -14 ; +ASSERT (-11 * x0) + (-4 * x1) + (7 * x2) + (-32 * x3) >= 31 ; +ASSERT (18 * x0) + (32 * x1) + (-24 * x2) + (-19 * x3) <= -6 ; +ASSERT (-15 * x0) + (23 * x1) + (-19 * x2) + (-12 * x3) < 2 ; +ASSERT (-21 * x0) + (-8 * x1) + (-30 * x2) + (31 * x3) >= -29 ; +ASSERT (5 * x0) + (-24 * x1) + (-21 * x2) + (-10 * x3) >= -8 ; +ASSERT (-31 * x0) + (-26 * x1) + (13 * x2) + (-7 * x3) <= -32 ; +ASSERT (-18 * x0) + (-11 * x1) + (9 * x2) + (6 * x3) >= 8; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-041.cvc b/test/regress/regress1/arith/arith-int-041.cvc new file mode 100644 index 000000000..a0c2dc0f9 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-041.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-31 * x0) + (8 * x1) + (16 * x2) + (5 * x3) >= 1 ; +ASSERT (-30 * x0) + (13 * x1) + (-17 * x2) + (13 * x3) < -24 ; +ASSERT (-16 * x0) + (-11 * x1) + (-32 * x2) + (-18 * x3) > -29 ; +ASSERT (32 * x0) + (-2 * x1) + (27 * x2) + (0 * x3) >= -1 ; +ASSERT (12 * x0) + (-17 * x1) + (21 * x2) + (-3 * x3) <= 1 ; +ASSERT (-26 * x0) + (29 * x1) + (-13 * x2) + (15 * x3) <= 2; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-043.cvc b/test/regress/regress1/arith/arith-int-043.cvc new file mode 100644 index 000000000..7efea85e5 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-043.cvc @@ -0,0 +1,9 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-21 * x0) + (-23 * x1) + (29 * x2) + (-4 * x3) = 25 ; +ASSERT (20 * x0) + (-19 * x1) + (3 * x2) + (-1 * x3) <= -8 ; +ASSERT (2 * x0) + (-22 * x1) + (-30 * x2) + (-9 * x3) >= 17 ; +ASSERT (21 * x0) + (5 * x1) + (-13 * x2) + (0 * x3) <= 18 ; +ASSERT (9 * x0) + (-5 * x1) + (30 * x2) + (17 * x3) > -12 ; +ASSERT (-2 * x0) + (-27 * x1) + (-5 * x2) + (-23 * x3) < 24; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-044.cvc b/test/regress/regress1/arith/arith-int-044.cvc new file mode 100644 index 000000000..f933b014b --- /dev/null +++ b/test/regress/regress1/arith/arith-int-044.cvc @@ -0,0 +1,10 @@ +% EXPECT: valid +%%%% down from 24, up from 6, up from 39 +x0, x1, x2, x3 : INT; +ASSERT (-30 * x0) + (18 * x1) + (17 * x2) + (3 * x3) = 0; +ASSERT (-25 * x0) + (-16 * x1) + (17 * x2) + (26 * x3) < 23 ; +ASSERT (-27 * x0) + (9 * x1) + (7 * x2) + (-24 * x3) < -27 ; +ASSERT (14 * x0) + (-27 * x1) + (-10 * x2) + (16 * x3) >= -23 ; +ASSERT (14 * x0) + (-27 * x1) + (-3 * x2) + (2 * x3) > -9 ; +ASSERT (-19 * x0) + (-9 * x1) + (-3 * x2) + (29 * x3) <= 5 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-045.cvc b/test/regress/regress1/arith/arith-int-045.cvc new file mode 100644 index 000000000..ca1a12ba6 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-045.cvc @@ -0,0 +1,9 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-22 * x0) + (-5 * x1) + (-5 * x2) + (25 * x3) = 22 ; +ASSERT (2 * x0) + (-25 * x1) + (4 * x2) + (-21 * x3) >= 0 ; +ASSERT (30 * x0) + (6 * x1) + (-17 * x2) + (-6 * x3) > 8 ; +ASSERT (28 * x0) + (-17 * x1) + (26 * x2) + (-1 * x3) >= 17 ; +ASSERT (2 * x0) + (-32 * x1) + (30 * x2) + (10 * x3) < -23 ; +ASSERT (22 * x0) + (-18 * x1) + (7 * x2) + (28 * x3) < -26; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-046.cvc b/test/regress/regress1/arith/arith-int-046.cvc new file mode 100644 index 000000000..d4d206c6e --- /dev/null +++ b/test/regress/regress1/arith/arith-int-046.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (2 * x0) + (-6 * x1) + (14 * x2) + (-24 * x3) > 4 ; +ASSERT (-13 * x0) + (-2 * x1) + (-9 * x2) + (-7 * x3) >= 29 ; +ASSERT (-11 * x0) + (28 * x1) + (-20 * x2) + (-2 * x3) >= 31; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-047.cvc b/test/regress/regress1/arith/arith-int-047.cvc new file mode 100644 index 000000000..0763e5dc3 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-047.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-14 * x0) + (27 * x1) + (10 * x2) + (1 * x3) = 10; +ASSERT (-29 * x0) + (-26 * x1) + (-16 * x2) + (17 * x3) >= 16 ; +ASSERT (-3 * x0) + (-2 * x1) + (26 * x2) + (30 * x3) < -27 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-048.cvc b/test/regress/regress1/arith/arith-int-048.cvc new file mode 100644 index 000000000..e7c05332d --- /dev/null +++ b/test/regress/regress1/arith/arith-int-048.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (-11 * x1) + (-14 * x2) + (21 * x3) = 6 ; +ASSERT (7 * x0) + (5 * x1) + (13 * x2) + (21 * x3) <= 27 ; +ASSERT (15 * x0) + (-11 * x1) + (-19 * x2) + (-13 * x3) < 5; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-049.cvc b/test/regress/regress1/arith/arith-int-049.cvc new file mode 100644 index 000000000..8eabc78a8 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-049.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-15 * x0) + (-20 * x1) + (-32 * x2) + (-16 * x3) = -19 ; +ASSERT (24 * x0) + (23 * x1) + (22 * x2) + (30 * x3) >= 19 ; +ASSERT (14 * x0) + (-6 * x1) + (28 * x2) + (-22 * x3) < -16; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-050.cvc b/test/regress/regress1/arith/arith-int-050.cvc new file mode 100644 index 000000000..f0ba939b7 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-050.cvc @@ -0,0 +1,6 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (-19 * x1) + (6 * x2) + (32 * x3) > 16 ; +ASSERT (-1 * x0) + (-30 * x1) + (15 * x2) + (7 * x3) < -10 ; +ASSERT (-13 * x0) + (24 * x1) + (27 * x2) + (20 * x3) < -5; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-051.cvc b/test/regress/regress1/arith/arith-int-051.cvc new file mode 100644 index 000000000..9a2497432 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-051.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (7 * x1) + (-3 * x2) + (9 * x3) = -3 ; +ASSERT (17 * x0) + (-22 * x1) + (-15 * x2) + (-21 * x3) >= 9 ; +ASSERT (-9 * x0) + (12 * x1) + (23 * x2) + (-24 * x3) >= -30 ; +ASSERT (-13 * x0) + (-3 * x1) + (-15 * x2) + (32 * x3) <= 26 ; +ASSERT (-27 * x0) + (9 * x1) + (-21 * x2) + (-5 * x3) < -9 ; +ASSERT (22 * x0) + (24 * x1) + (-10 * x2) + (-6 * x3) > -1 ; +ASSERT (20 * x0) + (-24 * x1) + (29 * x2) + (-21 * x3) <= 29 ; +ASSERT (25 * x0) + (11 * x1) + (8 * x2) + (-5 * x3) < -29 ; +ASSERT (-12 * x0) + (24 * x1) + (4 * x2) + (27 * x3) < 31; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-052.cvc b/test/regress/regress1/arith/arith-int-052.cvc new file mode 100644 index 000000000..83fdc89c8 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-052.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-25 * x0) + (-23 * x1) + (11 * x2) + (10 * x3) = 7 ; +ASSERT (32 * x0) + (-15 * x1) + (-1 * x2) + (29 * x3) > -25 ; +ASSERT (29 * x0) + (-8 * x1) + (22 * x2) + (20 * x3) < 14 ; +ASSERT (31 * x0) + (-16 * x1) + (-17 * x2) + (-21 * x3) >= 32 ; +ASSERT (-24 * x0) + (-29 * x1) + (9 * x2) + (14 * x3) <= -4 ; +ASSERT (13 * x0) + (13 * x1) + (14 * x2) + (5 * x3) <= 25 ; +ASSERT (5 * x0) + (12 * x1) + (-5 * x2) + (-9 * x3) >= -28 ; +ASSERT (27 * x0) + (19 * x1) + (6 * x2) + (25 * x3) >= -12 ; +ASSERT (24 * x0) + (-26 * x1) + (2 * x2) + (0 * x3) >= -25; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-053.cvc b/test/regress/regress1/arith/arith-int-053.cvc new file mode 100644 index 000000000..fa38fa3da --- /dev/null +++ b/test/regress/regress1/arith/arith-int-053.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-21 * x0) + (21 * x1) + (23 * x2) + (-20 * x3) = -8 ; +ASSERT (-31 * x0) + (-15 * x1) + (-23 * x2) + (29 * x3) = 17; +ASSERT (28 * x0) + (30 * x1) + (26 * x2) + (2 * x3) < 8 ; +ASSERT (17 * x0) + (-11 * x1) + (6 * x2) + (8 * x3) > 11 ; +ASSERT (20 * x0) + (-14 * x1) + (16 * x2) + (-3 * x3) < 9 ; +ASSERT (-11 * x0) + (2 * x1) + (4 * x2) + (-4 * x3) < -21 ; +ASSERT (25 * x0) + (6 * x1) + (-22 * x2) + (8 * x3) <= 7 ; +ASSERT (-8 * x0) + (9 * x1) + (-13 * x2) + (27 * x3) >= 0 ; +ASSERT (-16 * x0) + (-8 * x1) + (23 * x2) + (25 * x3) >= -13 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-054.cvc b/test/regress/regress1/arith/arith-int-054.cvc new file mode 100644 index 000000000..9b0066966 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-054.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-31 * x0) + (-29 * x1) + (6 * x2) + (8 * x3) = -10 ; +ASSERT (0 * x0) + (8 * x1) + (-20 * x2) + (12 * x3) = 16 ; +ASSERT (19 * x0) + (-30 * x1) + (8 * x2) + (-4 * x3) = -17 ; +ASSERT (-10 * x0) + (26 * x1) + (11 * x2) + (-31 * x3) = -26; +ASSERT (-22 * x0) + (15 * x1) + (14 * x2) + (3 * x3) <= -3 ; +ASSERT (-15 * x0) + (7 * x1) + (29 * x2) + (16 * x3) >= -6 ; +ASSERT (-20 * x0) + (20 * x1) + (31 * x2) + (-24 * x3) <= 14 ; +ASSERT (2 * x0) + (31 * x1) + (15 * x2) + (-1 * x3) >= -6 ; +ASSERT (-30 * x0) + (-11 * x1) + (26 * x2) + (6 * x3) >= -30 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-055.cvc b/test/regress/regress1/arith/arith-int-055.cvc new file mode 100644 index 000000000..9729fb565 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-055.cvc @@ -0,0 +1,12 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-21 * x0) + (-4 * x1) + (-28 * x2) + (-7 * x3) = -23 ; +ASSERT (-7 * x0) + (-21 * x1) + (29 * x2) + (11 * x3) = 29 ; +ASSERT (-26 * x0) + (-7 * x1) + (-25 * x2) + (-19 * x3) < -4 ; +ASSERT (4 * x0) + (14 * x1) + (-16 * x2) + (-32 * x3) >= -16 ; +ASSERT (10 * x0) + (-9 * x1) + (20 * x2) + (-27 * x3) <= 31 ; +ASSERT (29 * x0) + (16 * x1) + (25 * x2) + (-1 * x3) < -26 ; +ASSERT (-29 * x0) + (1 * x1) + (11 * x2) + (32 * x3) < 12 ; +ASSERT (-4 * x0) + (-22 * x1) + (0 * x2) + (-29 * x3) < 31 ; +ASSERT (12 * x0) + (-8 * x1) + (-17 * x2) + (-8 * x3) > 8; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-056.cvc b/test/regress/regress1/arith/arith-int-056.cvc new file mode 100644 index 000000000..e1c3ee1da --- /dev/null +++ b/test/regress/regress1/arith/arith-int-056.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-25 * x0) + (23 * x1) + (29 * x2) + (21 * x3) = -2 ; +ASSERT (1 * x0) + (10 * x1) + (-32 * x2) + (-17 * x3) = -2 ; +ASSERT (3 * x0) + (-32 * x1) + (-23 * x2) + (13 * x3) = 16 ; +ASSERT (25 * x0) + (-14 * x1) + (-17 * x2) + (16 * x3) <= 24 ; +ASSERT (1 * x0) + (-21 * x1) + (2 * x2) + (2 * x3) >= 15 ; +ASSERT (24 * x0) + (9 * x1) + (23 * x2) + (-2 * x3) >= -26 ; +%%ASSERT (-25 * x0) + (26 * x1) + (-3 * x2) + (-26 * x3) >= -20 ; +%%ASSERT (4 * x0) + (23 * x1) + (-24 * x2) + (7 * x3) <= -18 ; +%%ASSERT (-16 * x0) + (-24 * x1) + (26 * x2) + (1 * x3) > 15 ; +%%%%ASSERT (1 * x0) + (9 * x1) + (-18 * x2) + (11 * x3) > -3 ; +%%ASSERT (-9 * x0) + (20 * x1) + (15 * x2) + (4 * x3) < -17 ; +%%ASSERT (25 * x0) + (-22 * x1) + (-26 * x2) + (-21 * x3) > 17; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-057.cvc b/test/regress/regress1/arith/arith-int-057.cvc new file mode 100644 index 000000000..4e7b939b4 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-057.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-8 * x0) + (10 * x1) + (-25 * x2) + (-10 * x3) = -18 ; +ASSERT (27 * x0) + (5 * x1) + (8 * x2) + (13 * x3) = -8; +ASSERT (2 * x0) + (22 * x1) + (-13 * x2) + (16 * x3) <= 17 ; +ASSERT (18 * x0) + (18 * x1) + (15 * x2) + (-17 * x3) < -13 ; +ASSERT (-24 * x0) + (-8 * x1) + (31 * x2) + (-25 * x3) > 23 ; +ASSERT (-13 * x0) + (-22 * x1) + (11 * x2) + (28 * x3) >= -6 ; +ASSERT (20 * x0) + (-26 * x1) + (-20 * x2) + (-7 * x3) < -5 ; +ASSERT (-23 * x0) + (8 * x1) + (28 * x2) + (17 * x3) > 23 ; +ASSERT (32 * x0) + (31 * x1) + (-26 * x2) + (29 * x3) <= -1 ; +ASSERT (-2 * x0) + (-11 * x1) + (15 * x2) + (17 * x3) > -27 ; +ASSERT (-13 * x0) + (-30 * x1) + (-25 * x2) + (-18 * x3) <= 24 ; +ASSERT (23 * x0) + (-4 * x1) + (26 * x2) + (32 * x3) >= 23 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-058.cvc b/test/regress/regress1/arith/arith-int-058.cvc new file mode 100644 index 000000000..4d964f1c6 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-058.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-15 * x0) + (3 * x1) + (31 * x2) + (2 * x3) = -18 ; +ASSERT (-25 * x0) + (-10 * x1) + (15 * x2) + (29 * x3) = -18 ; +ASSERT (-17 * x0) + (31 * x1) + (-11 * x2) + (-29 * x3) = -2 ; +ASSERT (18 * x0) + (11 * x1) + (13 * x2) + (-16 * x3) >= 5 ; +ASSERT (-28 * x0) + (-30 * x1) + (13 * x2) + (-20 * x3) <= -19 ; +ASSERT (-10 * x0) + (-20 * x1) + (-13 * x2) + (-4 * x3) < 3 ; +ASSERT (-30 * x0) + (-5 * x1) + (-15 * x2) + (-1 * x3) > 19 ; +ASSERT (-8 * x0) + (28 * x1) + (17 * x2) + (23 * x3) <= 30 ; +ASSERT (-28 * x0) + (-16 * x1) + (-19 * x2) + (-23 * x3) >= 9 ; +ASSERT (-8 * x0) + (-15 * x1) + (-19 * x2) + (29 * x3) > -28 ; +ASSERT (-27 * x0) + (-12 * x1) + (-2 * x2) + (-29 * x3) >= -5 ; +ASSERT (32 * x0) + (-16 * x1) + (29 * x2) + (-12 * x3) < 26; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-059.cvc b/test/regress/regress1/arith/arith-int-059.cvc new file mode 100644 index 000000000..841d9c8e1 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-059.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (31 * x0) + (-19 * x1) + (0 * x2) + (32 * x3) = -14 ; +ASSERT (12 * x0) + (-25 * x1) + (-32 * x2) + (-18 * x3) = 18 ; +ASSERT (-6 * x0) + (-21 * x1) + (-11 * x2) + (-10 * x3) = 11 ; +ASSERT (22 * x0) + (-7 * x1) + (2 * x2) + (-16 * x3) = 16; +ASSERT (15 * x0) + (-14 * x1) + (29 * x2) + (24 * x3) >= 14 ; +ASSERT (-26 * x0) + (-6 * x1) + (-13 * x2) + (25 * x3) < -4 ; +ASSERT (-24 * x0) + (-22 * x1) + (-21 * x2) + (-6 * x3) > -21 ; +ASSERT (17 * x0) + (-21 * x1) + (25 * x2) + (-13 * x3) >= 16 ; +ASSERT (14 * x0) + (-25 * x1) + (-22 * x2) + (18 * x3) >= -30 ; +ASSERT (-27 * x0) + (8 * x1) + (-12 * x2) + (26 * x3) >= 15 ; +ASSERT (-31 * x0) + (2 * x1) + (19 * x2) + (-11 * x3) >= -27 ; +ASSERT (32 * x0) + (-29 * x1) + (9 * x2) + (-4 * x3) < 3 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-060.cvc b/test/regress/regress1/arith/arith-int-060.cvc new file mode 100644 index 000000000..227cb49b1 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-060.cvc @@ -0,0 +1,15 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (3 * x0) + (8 * x1) + (26 * x2) + (-17 * x3) = 31 ; +ASSERT (-14 * x0) + (25 * x1) + (4 * x2) + (-8 * x3) = 15 ; +ASSERT (-21 * x0) + (26 * x1) + (-10 * x2) + (-28 * x3) = 5; +ASSERT (2 * x0) + (-15 * x1) + (12 * x2) + (22 * x3) < -22 ; +ASSERT (10 * x0) + (24 * x1) + (11 * x2) + (-17 * x3) < 17 ; +ASSERT (26 * x0) + (32 * x1) + (-17 * x2) + (-3 * x3) >= 20 ; +ASSERT (11 * x0) + (26 * x1) + (-23 * x2) + (22 * x3) <= 32 ; +ASSERT (-19 * x0) + (22 * x1) + (-21 * x2) + (-28 * x3) <= -5 ; +ASSERT (-5 * x0) + (-18 * x1) + (10 * x2) + (-27 * x3) < -26 ; +ASSERT (21 * x0) + (-26 * x1) + (25 * x2) + (-13 * x3) < 15 ; +ASSERT (22 * x0) + (-2 * x1) + (3 * x2) + (-21 * x3) < 7 ; +ASSERT (20 * x0) + (-3 * x1) + (27 * x2) + (-21 * x3) < -18 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-061.cvc b/test/regress/regress1/arith/arith-int-061.cvc new file mode 100644 index 000000000..4a3cc28d0 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-061.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (16 * x0) + (20 * x1) + (-8 * x2) + (-27 * x3) = -2 ; +ASSERT (15 * x0) + (9 * x1) + (-1 * x2) + (4 * x3) = 1 ; +ASSERT (-25 * x0) + (19 * x1) + (-26 * x2) + (-20 * x3) = 22 ; +ASSERT (-11 * x0) + (28 * x1) + (-16 * x2) + (-15 * x3) = 15 ; +ASSERT (-11 * x0) + (-25 * x1) + (-16 * x2) + (25 * x3) = -3 ; +ASSERT (-15 * x0) + (-25 * x1) + (11 * x2) + (-24 * x3) = 29 ; +ASSERT (-12 * x0) + (-32 * x1) + (-28 * x2) + (-27 * x3) = -7 ; +ASSERT (16 * x0) + (5 * x1) + (10 * x2) + (-18 * x3) = 18 ; +ASSERT (-2 * x0) + (5 * x1) + (30 * x2) + (29 * x3) = -29 ; +ASSERT (-14 * x0) + (-20 * x1) + (21 * x2) + (1 * x3) = 31 ; +ASSERT (15 * x0) + (-7 * x1) + (-3 * x2) + (-24 * x3) > 3 ; +ASSERT (-16 * x0) + (-30 * x1) + (-31 * x2) + (16 * x3) > -9 ; +ASSERT (12 * x0) + (27 * x1) + (-11 * x2) + (-10 * x3) > -6 ; +ASSERT (0 * x0) + (29 * x1) + (32 * x2) + (9 * x3) <= -24 ; +ASSERT (11 * x0) + (-7 * x1) + (24 * x2) + (-30 * x3) >= 8 ; +ASSERT (1 * x0) + (25 * x1) + (29 * x2) + (15 * x3) <= -13 ; +ASSERT (-25 * x0) + (31 * x1) + (-32 * x2) + (-1 * x3) <= 9 ; +ASSERT (-22 * x0) + (-23 * x1) + (-4 * x2) + (-12 * x3) > 32 ; +ASSERT (22 * x0) + (-1 * x1) + (27 * x2) + (-22 * x3) > 20 ; +ASSERT (-20 * x0) + (-21 * x1) + (1 * x2) + (-32 * x3) >= 16; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-062.cvc b/test/regress/regress1/arith/arith-int-062.cvc new file mode 100644 index 000000000..f9a3156a2 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-062.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (11 * x0) + (22 * x1) + (19 * x2) + (-8 * x3) = 12 ; +ASSERT (23 * x0) + (-6 * x1) + (-5 * x2) + (26 * x3) = 0 ; +ASSERT (1 * x0) + (-23 * x1) + (22 * x2) + (10 * x3) = -18 ; +ASSERT (-13 * x0) + (-17 * x1) + (-8 * x2) + (-16 * x3) = 16 ; +ASSERT (24 * x0) + (-4 * x1) + (-26 * x2) + (9 * x3) = -26 ; +ASSERT (24 * x0) + (23 * x1) + (17 * x2) + (-10 * x3) >= 5 ; +ASSERT (-12 * x0) + (-12 * x1) + (-13 * x2) + (-22 * x3) <= 9 ; +ASSERT (-7 * x0) + (17 * x1) + (-24 * x2) + (-8 * x3) <= -31 ; +ASSERT (-28 * x0) + (-10 * x1) + (3 * x2) + (-23 * x3) <= -19 ; +ASSERT (12 * x0) + (-16 * x1) + (27 * x2) + (-28 * x3) > -27 ; +ASSERT (-15 * x0) + (-24 * x1) + (12 * x2) + (21 * x3) < 21 ; +ASSERT (6 * x0) + (31 * x1) + (5 * x2) + (-5 * x3) >= 10 ; +ASSERT (-7 * x0) + (-20 * x1) + (-9 * x2) + (-32 * x3) >= 7 ; +ASSERT (3 * x0) + (24 * x1) + (-18 * x2) + (-9 * x3) < -30 ; +ASSERT (-14 * x0) + (22 * x1) + (22 * x2) + (-22 * x3) < -16 ; +ASSERT (1 * x0) + (4 * x1) + (10 * x2) + (28 * x3) > -31 ; +ASSERT (-14 * x0) + (-15 * x1) + (-8 * x2) + (2 * x3) >= 3 ; +ASSERT (13 * x0) + (-27 * x1) + (-14 * x2) + (28 * x3) < 28 ; +ASSERT (26 * x0) + (-12 * x1) + (-21 * x2) + (-16 * x3) < -26 ; +ASSERT (-6 * x0) + (-19 * x1) + (-8 * x2) + (18 * x3) >= 27; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-063.cvc b/test/regress/regress1/arith/arith-int-063.cvc new file mode 100644 index 000000000..d88104688 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-063.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (20 * x0) + (-10 * x1) + (-10 * x2) + (26 * x3) = -9 ; +ASSERT (10 * x0) + (0 * x1) + (16 * x2) + (7 * x3) = 7 ; +ASSERT (6 * x0) + (-10 * x1) + (4 * x2) + (23 * x3) = 10; +ASSERT (-8 * x0) + (12 * x1) + (-19 * x2) + (-17 * x3) >= 21 ; +ASSERT (-20 * x0) + (6 * x1) + (-12 * x2) + (-31 * x3) > -31 ; +ASSERT (32 * x0) + (-6 * x1) + (-14 * x2) + (-32 * x3) >= 13 ; +ASSERT (29 * x0) + (12 * x1) + (17 * x2) + (9 * x3) > 32 ; +ASSERT (1 * x0) + (21 * x1) + (12 * x2) + (23 * x3) <= 14 ; +ASSERT (-12 * x0) + (-9 * x1) + (26 * x2) + (26 * x3) < 3 ; +ASSERT (-8 * x0) + (27 * x1) + (29 * x2) + (-10 * x3) >= 22 ; +ASSERT (-15 * x0) + (29 * x1) + (29 * x2) + (17 * x3) <= 22 ; +ASSERT (-4 * x0) + (0 * x1) + (1 * x2) + (-24 * x3) < -24 ; +ASSERT (25 * x0) + (17 * x1) + (31 * x2) + (-28 * x3) >= -12 ; +ASSERT (32 * x0) + (8 * x1) + (-3 * x2) + (19 * x3) > -19 ; +ASSERT (-27 * x0) + (-18 * x1) + (18 * x2) + (22 * x3) > 26 ; +ASSERT (29 * x0) + (29 * x1) + (4 * x2) + (-6 * x3) >= 8 ; +ASSERT (-12 * x0) + (17 * x1) + (-22 * x2) + (1 * x3) < 30 ; +ASSERT (-24 * x0) + (16 * x1) + (-26 * x2) + (-27 * x3) > 29 ; +ASSERT (9 * x0) + (15 * x1) + (-28 * x2) + (0 * x3) > -2 ; +ASSERT (-5 * x0) + (30 * x1) + (-21 * x2) + (-6 * x3) >= 12 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-064.cvc b/test/regress/regress1/arith/arith-int-064.cvc new file mode 100644 index 000000000..21ca822e1 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-064.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-8 * x0) + (-11 * x1) + (27 * x2) + (4 * x3) = 6 ; +ASSERT (32 * x0) + (27 * x1) + (31 * x2) + (-13 * x3) = 21 ; +ASSERT (-6 * x0) + (17 * x1) + (-20 * x2) + (11 * x3) < -5 ; +ASSERT (15 * x0) + (-15 * x1) + (-13 * x2) + (-21 * x3) < 27 ; +ASSERT (-24 * x0) + (-22 * x1) + (5 * x2) + (22 * x3) < 23 ; +ASSERT (27 * x0) + (23 * x1) + (-19 * x2) + (20 * x3) >= -8 ; +ASSERT (27 * x0) + (-27 * x1) + (23 * x2) + (17 * x3) < -5 ; +ASSERT (-11 * x0) + (-8 * x1) + (14 * x2) + (-10 * x3) <= 1 ; +ASSERT (12 * x0) + (7 * x1) + (-26 * x2) + (-28 * x3) >= -7 ; +ASSERT (25 * x0) + (-25 * x1) + (5 * x2) + (32 * x3) > -10 ; +ASSERT (-29 * x0) + (-24 * x1) + (26 * x2) + (-31 * x3) < -16 ; +ASSERT (10 * x0) + (29 * x1) + (9 * x2) + (23 * x3) < 13 ; +ASSERT (-26 * x0) + (6 * x1) + (-14 * x2) + (-21 * x3) > -15 ; +ASSERT (24 * x0) + (-14 * x1) + (-32 * x2) + (22 * x3) > -31 ; +ASSERT (-31 * x0) + (-16 * x1) + (-9 * x2) + (-32 * x3) > -19 ; +ASSERT (-1 * x0) + (17 * x1) + (26 * x2) + (-16 * x3) > -27 ; +ASSERT (10 * x0) + (-11 * x1) + (-20 * x2) + (-25 * x3) < -30 ; +ASSERT (-16 * x0) + (9 * x1) + (-10 * x2) + (-8 * x3) < -9 ; +ASSERT (19 * x0) + (10 * x1) + (18 * x2) + (7 * x3) < -30 ; +ASSERT (20 * x0) + (-25 * x1) + (-18 * x2) + (-2 * x3) <= -11; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-065.cvc b/test/regress/regress1/arith/arith-int-065.cvc new file mode 100644 index 000000000..b1b9e1b51 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-065.cvc @@ -0,0 +1,23 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (3 * x0) + (-21 * x1) + (-3 * x2) + (6 * x3) = -18 ; +ASSERT (-15 * x0) + (19 * x1) + (-21 * x2) + (-29 * x3) = -8 ; +ASSERT (32 * x0) + (-2 * x1) + (14 * x2) + (5 * x3) = -15 ; +ASSERT (-16 * x0) + (22 * x1) + (0 * x2) + (-26 * x3) >= 18 ; +ASSERT (11 * x0) + (-19 * x1) + (10 * x2) + (26 * x3) >= -20 ; +ASSERT (-25 * x0) + (-24 * x1) + (12 * x2) + (4 * x3) >= -14 ; +ASSERT (-20 * x0) + (-10 * x1) + (21 * x2) + (23 * x3) >= 28 ; +ASSERT (6 * x0) + (-31 * x1) + (11 * x2) + (-3 * x3) <= 4 ; +ASSERT (2 * x0) + (11 * x1) + (-13 * x2) + (-16 * x3) >= 23 ; +ASSERT (-6 * x0) + (-24 * x1) + (24 * x2) + (7 * x3) <= 14 ; +ASSERT (0 * x0) + (3 * x1) + (-14 * x2) + (-19 * x3) >= 15 ; +ASSERT (-31 * x0) + (-27 * x1) + (-32 * x2) + (-28 * x3) <= -15 ; +ASSERT (-11 * x0) + (3 * x1) + (-6 * x2) + (-5 * x3) < -31 ; +ASSERT (-2 * x0) + (-21 * x1) + (2 * x2) + (28 * x3) >= 7 ; +ASSERT (-12 * x0) + (19 * x1) + (-17 * x2) + (-14 * x3) > 11 ; +ASSERT (32 * x0) + (-29 * x1) + (-12 * x2) + (24 * x3) < -9 ; +ASSERT (-19 * x0) + (1 * x1) + (8 * x2) + (4 * x3) <= 3 ; +ASSERT (13 * x0) + (17 * x1) + (22 * x2) + (13 * x3) <= -25 ; +ASSERT (2 * x0) + (-4 * x1) + (-3 * x2) + (19 * x3) <= -12 ; +ASSERT (-16 * x0) + (-20 * x1) + (21 * x2) + (-30 * x3) <= 2; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-066.cvc b/test/regress/regress1/arith/arith-int-066.cvc new file mode 100644 index 000000000..9532b4198 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-066.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (28 * x0) + (-8 * x1) + (32 * x2) + (-3 * x3) = -18 ; +ASSERT (-4 * x0) + (5 * x1) + (-2 * x2) + (-17 * x3) > 19 ; +ASSERT (-9 * x0) + (14 * x1) + (-16 * x2) + (15 * x3) > 18 ; +ASSERT (-28 * x0) + (-25 * x1) + (-10 * x2) + (-10 * x3) < -10 ; +ASSERT (19 * x0) + (-4 * x1) + (11 * x2) + (22 * x3) <= -6 ; +ASSERT (2 * x0) + (32 * x1) + (-16 * x2) + (-29 * x3) > 6 ; +ASSERT (-7 * x0) + (9 * x1) + (-25 * x2) + (6 * x3) <= 5 ; +ASSERT (4 * x0) + (-18 * x1) + (-21 * x2) + (12 * x3) >= -32 ; +ASSERT (-27 * x0) + (11 * x1) + (-3 * x2) + (-6 * x3) < 1 ; +ASSERT (10 * x0) + (13 * x1) + (11 * x2) + (28 * x3) > -15 ; +ASSERT (-1 * x0) + (-4 * x1) + (30 * x2) + (6 * x3) > 9 ; +ASSERT (19 * x0) + (14 * x1) + (17 * x2) + (-8 * x3) <= -21 ; +ASSERT (-15 * x0) + (20 * x1) + (9 * x2) + (19 * x3) <= 4 ; +ASSERT (-9 * x0) + (-22 * x1) + (29 * x2) + (-6 * x3) <= 3; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-067.cvc b/test/regress/regress1/arith/arith-int-067.cvc new file mode 100644 index 000000000..5d7b52e69 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-067.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-25 * x0) + (-32 * x1) + (-29 * x2) + (-9 * x3) = -2 ; +ASSERT (22 * x0) + (10 * x1) + (-18 * x2) + (2 * x3) = -17 ; +ASSERT (22 * x0) + (6 * x1) + (-9 * x2) + (27 * x3) = 10 ; +ASSERT (1 * x0) + (-26 * x1) + (27 * x2) + (-19 * x3) = 29 ; +ASSERT (-13 * x0) + (18 * x1) + (5 * x2) + (22 * x3) < -10 ; +ASSERT (5 * x0) + (1 * x1) + (4 * x2) + (-7 * x3) > -12 ; +ASSERT (-30 * x0) + (-12 * x1) + (-22 * x2) + (-32 * x3) <= 1 ; +ASSERT (-15 * x0) + (19 * x1) + (22 * x2) + (-9 * x3) >= 12 ; +ASSERT (-6 * x0) + (-16 * x1) + (30 * x2) + (-13 * x3) <= -9 ; +ASSERT (-3 * x0) + (1 * x1) + (10 * x2) + (7 * x3) < -32 ; +ASSERT (5 * x0) + (-17 * x1) + (25 * x2) + (-31 * x3) >= -6 ; +ASSERT (18 * x0) + (28 * x1) + (-6 * x2) + (10 * x3) <= -31 ; +ASSERT (-11 * x0) + (-25 * x1) + (2 * x2) + (-3 * x3) > -3 ; +ASSERT (-14 * x0) + (-28 * x1) + (-2 * x2) + (20 * x3) < -25; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-068.cvc b/test/regress/regress1/arith/arith-int-068.cvc new file mode 100644 index 000000000..107a21a12 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-068.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (-8 * x1) + (5 * x2) + (-7 * x3) = -7 ; +ASSERT (-30 * x0) + (24 * x1) + (-4 * x2) + (-30 * x3) = 22 ; +ASSERT (31 * x0) + (-32 * x1) + (27 * x2) + (29 * x3) = 23 ; +ASSERT (8 * x0) + (-19 * x1) + (-7 * x2) + (0 * x3) <= -1 ; +ASSERT (-32 * x0) + (30 * x1) + (9 * x2) + (-21 * x3) <= 24 ; +ASSERT (15 * x0) + (-4 * x1) + (27 * x2) + (-26 * x3) >= 23 ; +ASSERT (7 * x0) + (26 * x1) + (-16 * x2) + (21 * x3) >= 16 ; +ASSERT (-24 * x0) + (-17 * x1) + (-9 * x2) + (27 * x3) <= 2 ; +ASSERT (29 * x0) + (-7 * x1) + (-8 * x2) + (32 * x3) <= -2 ; +ASSERT (32 * x0) + (31 * x1) + (7 * x2) + (-26 * x3) < 1 ; +ASSERT (-17 * x0) + (-13 * x1) + (-20 * x2) + (29 * x3) >= -21 ; +ASSERT (-32 * x0) + (27 * x1) + (-29 * x2) + (-11 * x3) >= -23 ; +ASSERT (29 * x0) + (-4 * x1) + (21 * x2) + (-16 * x3) < 23 ; +ASSERT (-15 * x0) + (26 * x1) + (14 * x2) + (13 * x3) <= -29; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-069.cvc b/test/regress/regress1/arith/arith-int-069.cvc new file mode 100644 index 000000000..3fab229b0 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-069.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-12 * x0) + (20 * x1) + (2 * x2) + (-24 * x3) = 16 ; +ASSERT (-32 * x0) + (27 * x1) + (1 * x2) + (-3 * x3) = -3 ; +ASSERT (13 * x0) + (27 * x1) + (-17 * x2) + (25 * x3) <= -17 ; +ASSERT (27 * x0) + (-30 * x1) + (-16 * x2) + (-3 * x3) > -19 ; +ASSERT (-18 * x0) + (-25 * x1) + (-5 * x2) + (3 * x3) < -10 ; +ASSERT (9 * x0) + (-32 * x1) + (30 * x2) + (11 * x3) >= 23 ; +ASSERT (14 * x0) + (18 * x1) + (-21 * x2) + (-19 * x3) > 9 ; +ASSERT (28 * x0) + (2 * x1) + (23 * x2) + (17 * x3) < -6 ; +ASSERT (13 * x0) + (-17 * x1) + (-1 * x2) + (29 * x3) < -22 ; +ASSERT (-19 * x0) + (22 * x1) + (6 * x2) + (12 * x3) <= -9 ; +ASSERT (24 * x0) + (-14 * x1) + (31 * x2) + (12 * x3) > -26 ; +ASSERT (-1 * x0) + (24 * x1) + (-1 * x2) + (-31 * x3) > -21 ; +ASSERT (-22 * x0) + (28 * x1) + (-27 * x2) + (0 * x3) >= 3 ; +ASSERT (-28 * x0) + (29 * x1) + (-3 * x2) + (-22 * x3) >= -23; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-070.cvc b/test/regress/regress1/arith/arith-int-070.cvc new file mode 100644 index 000000000..cd828da5f --- /dev/null +++ b/test/regress/regress1/arith/arith-int-070.cvc @@ -0,0 +1,17 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (0 * x0) + (-16 * x1) + (14 * x2) + (20 * x3) = 1 ; +ASSERT (-27 * x0) + (-5 * x1) + (-22 * x2) + (-24 * x3) = -7 ; +ASSERT (-3 * x0) + (-28 * x1) + (-15 * x2) + (7 * x3) = -9 ; +ASSERT (27 * x0) + (4 * x1) + (-31 * x2) + (-32 * x3) <= -12 ; +ASSERT (16 * x0) + (6 * x1) + (17 * x2) + (22 * x3) <= 5 ; +ASSERT (-27 * x0) + (-16 * x1) + (1 * x2) + (23 * x3) >= 9 ; +ASSERT (21 * x0) + (-28 * x1) + (-26 * x2) + (-26 * x3) <= -25 ; +ASSERT (-12 * x0) + (-32 * x1) + (-22 * x2) + (-20 * x3) > -32 ; +ASSERT (26 * x0) + (26 * x1) + (30 * x2) + (4 * x3) < 21 ; +ASSERT (-22 * x0) + (-21 * x1) + (0 * x2) + (30 * x3) < 13 ; +ASSERT (13 * x0) + (17 * x1) + (-7 * x2) + (-31 * x3) < 29 ; +ASSERT (-12 * x0) + (30 * x1) + (1 * x2) + (4 * x3) > -24 ; +ASSERT (-23 * x0) + (-2 * x1) + (29 * x2) + (11 * x3) > 26 ; +ASSERT (-18 * x0) + (-16 * x1) + (31 * x2) + (14 * x3) <= 32; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-071.cvc b/test/regress/regress1/arith/arith-int-071.cvc new file mode 100644 index 000000000..ce5336476 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-071.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (3 * x1) + (-17 * x2) + (-21 * x3) = -9 ; +ASSERT (-12 * x0) + (-9 * x1) + (-9 * x2) + (-16 * x3) = -12 ; +ASSERT (-5 * x0) + (16 * x1) + (-15 * x2) + (-13 * x3) > 27 ; +ASSERT (16 * x0) + (-4 * x1) + (17 * x2) + (-24 * x3) > -9 ; +ASSERT (3 * x0) + (13 * x1) + (-15 * x2) + (-13 * x3) <= -32 ; +ASSERT (-18 * x0) + (21 * x1) + (-7 * x2) + (2 * x3) >= 13 ; +ASSERT (5 * x0) + (11 * x1) + (-11 * x2) + (-11 * x3) <= 9 ; +ASSERT (-9 * x0) + (8 * x1) + (-25 * x2) + (-14 * x3) >= 10 ; +ASSERT (17 * x0) + (-29 * x1) + (23 * x2) + (7 * x3) <= -31 ; +ASSERT (20 * x0) + (0 * x1) + (1 * x2) + (-6 * x3) <= 23 ; +ASSERT (-25 * x0) + (0 * x1) + (-32 * x2) + (17 * x3) > -14 ; +ASSERT (6 * x0) + (-30 * x1) + (-11 * x2) + (29 * x3) < 28 ; +ASSERT (-19 * x0) + (23 * x1) + (-19 * x2) + (3 * x3) >= 7 ; +ASSERT (29 * x0) + (21 * x1) + (-28 * x2) + (-28 * x3) < 22 ; +ASSERT (28 * x0) + (25 * x1) + (2 * x2) + (-23 * x3) <= -28; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-072.cvc b/test/regress/regress1/arith/arith-int-072.cvc new file mode 100644 index 000000000..10222deae --- /dev/null +++ b/test/regress/regress1/arith/arith-int-072.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (1 * x0) + (-1 * x1) + (-16 * x2) + (6 * x3) = -11 ; +ASSERT (-17 * x0) + (17 * x1) + (-15 * x2) + (24 * x3) = -21 ; +ASSERT (-31 * x0) + (28 * x1) + (-4 * x2) + (31 * x3) = -32 ; +ASSERT (1 * x0) + (-12 * x1) + (29 * x2) + (-6 * x3) = 25 ; +ASSERT (2 * x0) + (7 * x1) + (-24 * x2) + (28 * x3) >= -12 ; +ASSERT (-23 * x0) + (-22 * x1) + (14 * x2) + (-24 * x3) >= 22 ; +ASSERT (23 * x0) + (-21 * x1) + (22 * x2) + (26 * x3) >= -4 ; +ASSERT (25 * x0) + (27 * x1) + (14 * x2) + (5 * x3) <= 9 ; +ASSERT (16 * x0) + (2 * x1) + (24 * x2) + (-11 * x3) < -32 ; +ASSERT (0 * x0) + (23 * x1) + (29 * x2) + (-15 * x3) < -14 ; +ASSERT (5 * x0) + (-12 * x1) + (-7 * x2) + (29 * x3) <= -16 ; +ASSERT (25 * x0) + (26 * x1) + (14 * x2) + (-2 * x3) <= 13 ; +ASSERT (-30 * x0) + (19 * x1) + (24 * x2) + (7 * x3) < -23 ; +ASSERT (24 * x0) + (28 * x1) + (12 * x2) + (-25 * x3) >= -22 ; +ASSERT (27 * x0) + (-13 * x1) + (-16 * x2) + (-3 * x3) < 24; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-073.cvc b/test/regress/regress1/arith/arith-int-073.cvc new file mode 100644 index 000000000..98e74be8f --- /dev/null +++ b/test/regress/regress1/arith/arith-int-073.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (8 * x0) + (-14 * x1) + (0 * x2) + (7 * x3) = 26 ; +ASSERT (-7 * x0) + (-14 * x1) + (15 * x2) + (31 * x3) = 8 ; +ASSERT (-4 * x0) + (16 * x1) + (3 * x2) + (-1 * x3) = 12 ; +ASSERT (2 * x0) + (24 * x1) + (-7 * x2) + (4 * x3) = 24 ; +ASSERT (26 * x0) + (-8 * x1) + (28 * x2) + (9 * x3) = -12 ; +ASSERT (19 * x0) + (-3 * x1) + (25 * x2) + (10 * x3) <= -19 ; +ASSERT (-13 * x0) + (-16 * x1) + (-14 * x2) + (8 * x3) <= 25 ; +ASSERT (-21 * x0) + (-2 * x1) + (-20 * x2) + (8 * x3) <= -22 ; +ASSERT (16 * x0) + (4 * x1) + (11 * x2) + (-15 * x3) >= -12 ; +ASSERT (-24 * x0) + (-8 * x1) + (2 * x2) + (-24 * x3) <= -22 ; +ASSERT (29 * x0) + (23 * x1) + (-20 * x2) + (8 * x3) > 21 ; +ASSERT (-24 * x0) + (-28 * x1) + (-23 * x2) + (-24 * x3) < -5 ; +ASSERT (-1 * x0) + (17 * x1) + (19 * x2) + (-7 * x3) > -5 ; +ASSERT (24 * x0) + (3 * x1) + (6 * x2) + (10 * x3) <= 15 ; +ASSERT (27 * x0) + (-11 * x1) + (-8 * x2) + (-22 * x3) > -30; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-074.cvc b/test/regress/regress1/arith/arith-int-074.cvc new file mode 100644 index 000000000..28cc48186 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-074.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (14 * x0) + (-6 * x1) + (-23 * x2) + (-8 * x3) = -18 ; +ASSERT (-11 * x0) + (12 * x1) + (8 * x2) + (-1 * x3) = -32 ; +ASSERT (24 * x0) + (-10 * x1) + (19 * x2) + (7 * x3) = -30 ; +ASSERT (1 * x0) + (-12 * x1) + (-13 * x2) + (-17 * x3) = -28 ; +ASSERT (-17 * x0) + (14 * x1) + (7 * x2) + (-18 * x3) = -14 ; +ASSERT (7 * x0) + (14 * x1) + (-22 * x2) + (29 * x3) = -6; +ASSERT (15 * x0) + (-6 * x1) + (3 * x2) + (-19 * x3) > 26 ; +ASSERT (-20 * x0) + (-18 * x1) + (-24 * x2) + (5 * x3) >= -1 ; +ASSERT (11 * x0) + (-26 * x1) + (-20 * x2) + (-16 * x3) > -7 ; +ASSERT (31 * x0) + (-2 * x1) + (6 * x2) + (32 * x3) > -22 ; +ASSERT (-25 * x0) + (26 * x1) + (-26 * x2) + (-21 * x3) >= -27 ; +ASSERT (-17 * x0) + (-30 * x1) + (14 * x2) + (17 * x3) <= -19 ; +ASSERT (-16 * x0) + (4 * x1) + (1 * x2) + (-24 * x3) <= -24 ; +ASSERT (-13 * x0) + (29 * x1) + (-27 * x2) + (12 * x3) < -15 ; +ASSERT (26 * x0) + (-2 * x1) + (-28 * x2) + (20 * x3) < -20 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-075.cvc b/test/regress/regress1/arith/arith-int-075.cvc new file mode 100644 index 000000000..3b5131e8b --- /dev/null +++ b/test/regress/regress1/arith/arith-int-075.cvc @@ -0,0 +1,18 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-8 * x0) + (29 * x1) + (15 * x2) + (32 * x3) = 32 ; +ASSERT (18 * x0) + (-8 * x1) + (18 * x2) + (22 * x3) = 20 ; +ASSERT (11 * x0) + (9 * x1) + (32 * x2) + (-15 * x3) > 21 ; +ASSERT (12 * x0) + (1 * x1) + (25 * x2) + (-17 * x3) > -13 ; +ASSERT (-20 * x0) + (7 * x1) + (13 * x2) + (-15 * x3) <= -3 ; +ASSERT (32 * x0) + (4 * x1) + (-30 * x2) + (13 * x3) <= -15 ; +ASSERT (-32 * x0) + (-27 * x1) + (20 * x2) + (22 * x3) <= -28 ; +ASSERT (28 * x0) + (23 * x1) + (10 * x2) + (20 * x3) < 9 ; +ASSERT (-30 * x0) + (-32 * x1) + (-28 * x2) + (-30 * x3) > 17 ; +ASSERT (-26 * x0) + (14 * x1) + (30 * x2) + (31 * x3) < 20 ; +ASSERT (21 * x0) + (23 * x1) + (-7 * x2) + (-16 * x3) > -19 ; +ASSERT (6 * x0) + (0 * x1) + (0 * x2) + (21 * x3) < -1 ; +ASSERT (13 * x0) + (29 * x1) + (17 * x2) + (-29 * x3) < -32 ; +ASSERT (22 * x0) + (-9 * x1) + (-25 * x2) + (11 * x3) > 29 ; +ASSERT (-25 * x0) + (-19 * x1) + (22 * x2) + (-27 * x3) >= 10; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-076.cvc b/test/regress/regress1/arith/arith-int-076.cvc new file mode 100644 index 000000000..2c8de7cdf --- /dev/null +++ b/test/regress/regress1/arith/arith-int-076.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (0 * x1) + (4 * x2) + (29 * x3) = -15 ; +ASSERT (3 * x0) + (19 * x1) + (21 * x2) + (-32 * x3) = 11 ; +ASSERT (-23 * x0) + (-8 * x1) + (-12 * x2) + (-14 * x3) >= -25 ; +ASSERT (13 * x0) + (30 * x1) + (-12 * x2) + (22 * x3) < -12 ; +ASSERT (-12 * x0) + (-17 * x1) + (20 * x2) + (14 * x3) > -26 ; +ASSERT (-13 * x0) + (-17 * x1) + (-25 * x2) + (27 * x3) <= -29 ; +ASSERT (-8 * x0) + (-31 * x1) + (-3 * x2) + (-22 * x3) > -22 ; +ASSERT (30 * x0) + (11 * x1) + (-32 * x2) + (32 * x3) >= 28; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-077.cvc b/test/regress/regress1/arith/arith-int-077.cvc new file mode 100644 index 000000000..d14da386e --- /dev/null +++ b/test/regress/regress1/arith/arith-int-077.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (26 * x0) + (-28 * x1) + (27 * x2) + (8 * x3) = 31 ; +ASSERT (-32 * x0) + (11 * x1) + (-5 * x2) + (14 * x3) = 2; +ASSERT (3 * x0) + (17 * x1) + (30 * x2) + (31 * x3) < 13 ; +ASSERT (-17 * x0) + (-21 * x1) + (10 * x2) + (8 * x3) > 23 ; +ASSERT (-14 * x0) + (10 * x1) + (11 * x2) + (27 * x3) > -13 ; +ASSERT (-14 * x0) + (24 * x1) + (3 * x2) + (-26 * x3) > 1 ; +ASSERT (-14 * x0) + (20 * x1) + (-2 * x2) + (-24 * x3) > -26 ; +ASSERT (20 * x0) + (-23 * x1) + (30 * x2) + (-30 * x3) < 24 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-078.cvc b/test/regress/regress1/arith/arith-int-078.cvc new file mode 100644 index 000000000..3197c6524 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-078.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (17 * x0) + (-14 * x1) + (13 * x2) + (13 * x3) = -18 ; +ASSERT (13 * x0) + (16 * x1) + (-12 * x2) + (19 * x3) = -20 ; +ASSERT (-28 * x0) + (20 * x1) + (-9 * x2) + (9 * x3) = -3 ; +ASSERT (24 * x0) + (22 * x1) + (24 * x2) + (20 * x3) = 5; +ASSERT (-1 * x0) + (-12 * x1) + (20 * x2) + (26 * x3) >= 22 ; +ASSERT (-23 * x0) + (-20 * x1) + (-8 * x2) + (1 * x3) < 2 ; +ASSERT (5 * x0) + (-27 * x1) + (-24 * x2) + (25 * x3) > -21 ; +ASSERT (1 * x0) + (-8 * x1) + (-17 * x2) + (-27 * x3) < -24 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-080.cvc b/test/regress/regress1/arith/arith-int-080.cvc new file mode 100644 index 000000000..8be0f9a73 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-080.cvc @@ -0,0 +1,11 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (5 * x0) + (-17 * x1) + (15 * x2) + (-15 * x3) = -14 ; +ASSERT (-28 * x0) + (-17 * x1) + (-29 * x2) + (-19 * x3) = 14; +ASSERT (9 * x0) + (-26 * x1) + (-16 * x2) + (-9 * x3) >= 28 ; +ASSERT (14 * x0) + (-32 * x1) + (-31 * x2) + (0 * x3) >= 30 ; +ASSERT (-31 * x0) + (-27 * x1) + (23 * x2) + (4 * x3) >= 21 ; +ASSERT (27 * x0) + (-30 * x1) + (8 * x2) + (13 * x3) < 31 ; +ASSERT (-1 * x0) + (-29 * x1) + (23 * x2) + (10 * x3) < -10 ; +ASSERT (15 * x0) + (-2 * x1) + (22 * x2) + (-28 * x3) >= 2 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-081.cvc b/test/regress/regress1/arith/arith-int-081.cvc new file mode 100644 index 000000000..546148376 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-081.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-8 * x0) + (31 * x1) + (-23 * x2) + (-8 * x3) = 8; +ASSERT (24 * x0) + (-2 * x1) + (2 * x2) + (-2 * x3) >= -17 ; +ASSERT (-6 * x0) + (17 * x1) + (27 * x2) + (26 * x3) >= -30 ; +ASSERT (-19 * x0) + (-15 * x1) + (5 * x2) + (-27 * x3) < -3 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-082.cvc b/test/regress/regress1/arith/arith-int-082.cvc new file mode 100644 index 000000000..62bd45de7 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-082.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-29 * x0) + (-3 * x1) + (27 * x2) + (13 * x3) = -10 ; +ASSERT (7 * x0) + (-17 * x1) + (11 * x2) + (-30 * x3) <= 6 ; +ASSERT (30 * x0) + (17 * x1) + (-3 * x2) + (-31 * x3) > 10 ; +ASSERT (2 * x0) + (9 * x1) + (9 * x2) + (-16 * x3) <= 11; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-083.cvc b/test/regress/regress1/arith/arith-int-083.cvc new file mode 100644 index 000000000..6b1084353 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-083.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (19 * x0) + (-31 * x1) + (31 * x2) + (28 * x3) = -13 ; +ASSERT (1 * x0) + (13 * x1) + (12 * x2) + (-15 * x3) > -8 ; +ASSERT (7 * x0) + (17 * x1) + (-20 * x2) + (13 * x3) > -26 ; +ASSERT (-17 * x0) + (14 * x1) + (-23 * x2) + (17 * x3) <= -27; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-084.cvc b/test/regress/regress1/arith/arith-int-084.cvc new file mode 100644 index 000000000..5f0e17afe --- /dev/null +++ b/test/regress/regress1/arith/arith-int-084.cvc @@ -0,0 +1,7 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-2 * x0) + (-13 * x1) + (-14 * x2) + (-26 * x3) <= 4 ; +ASSERT (-17 * x0) + (-17 * x1) + (21 * x2) + (-4 * x3) < 18 ; +ASSERT (-31 * x0) + (23 * x1) + (4 * x2) + (29 * x3) > -6 ; +ASSERT (-14 * x0) + (32 * x1) + (-8 * x2) + (-8 * x3) <= -1; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-085.cvc b/test/regress/regress1/arith/arith-int-085.cvc new file mode 100644 index 000000000..74dd714e8 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-085.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +%% down from 3 +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (-25 * x1) + (-20 * x2) + (8 * x3) = -6 ; +ASSERT (-9 * x0) + (30 * x1) + (-17 * x2) + (29 * x3) >= -15 ; +ASSERT (21 * x0) + (29 * x1) + (12 * x2) + (-3 * x3) <= -21 ; +ASSERT (-16 * x0) + (-26 * x1) + (11 * x2) + (-12 * x3) >= -14; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-086.cvc b/test/regress/regress1/arith/arith-int-086.cvc new file mode 100644 index 000000000..64c212b3c --- /dev/null +++ b/test/regress/regress1/arith/arith-int-086.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-16 * x0) + (28 * x1) + (2 * x2) + (7 * x3) = -25 ; +ASSERT (-20 * x0) + (-24 * x1) + (4 * x2) + (32 * x3) = -22 ; +ASSERT (19 * x0) + (28 * x1) + (-15 * x2) + (18 * x3) < -9 ; +ASSERT (-10 * x0) + (1 * x1) + (-3 * x2) + (6 * x3) <= 1 ; +ASSERT (-15 * x0) + (-32 * x1) + (28 * x2) + (6 * x3) >= -8 ; +ASSERT (-18 * x0) + (-16 * x1) + (15 * x2) + (-28 * x3) <= 1 ; +ASSERT (-20 * x0) + (-31 * x1) + (20 * x2) + (13 * x3) >= -7 ; +ASSERT (29 * x0) + (16 * x1) + (7 * x2) + (14 * x3) < 11 ; +ASSERT (-10 * x0) + (22 * x1) + (25 * x2) + (24 * x3) >= 5 ; +ASSERT (-3 * x0) + (11 * x1) + (27 * x2) + (11 * x3) <= 9; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-087.cvc b/test/regress/regress1/arith/arith-int-087.cvc new file mode 100644 index 000000000..312c08917 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-087.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-4 * x0) + (25 * x1) + (-2 * x2) + (-16 * x3) = 27 ; +ASSERT (-11 * x0) + (26 * x1) + (18 * x2) + (-18 * x3) = -15 ; +ASSERT (-19 * x0) + (-27 * x1) + (-31 * x2) + (15 * x3) = 12; +ASSERT (10 * x0) + (-10 * x1) + (25 * x2) + (-3 * x3) < -30 ; +ASSERT (5 * x0) + (-18 * x1) + (21 * x2) + (-28 * x3) <= -4 ; +ASSERT (-6 * x0) + (15 * x1) + (-10 * x2) + (0 * x3) < -20 ; +ASSERT (10 * x0) + (23 * x1) + (-20 * x2) + (12 * x3) >= -15 ; +ASSERT (-31 * x0) + (-30 * x1) + (12 * x2) + (11 * x3) > 29 ; +ASSERT (26 * x0) + (23 * x1) + (28 * x2) + (-5 * x3) > 8 ; +ASSERT (6 * x0) + (-29 * x1) + (12 * x2) + (16 * x3) < 27 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-088.cvc b/test/regress/regress1/arith/arith-int-088.cvc new file mode 100644 index 000000000..5212640be --- /dev/null +++ b/test/regress/regress1/arith/arith-int-088.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-19 * x0) + (-9 * x1) + (-27 * x2) + (9 * x3) = -1 ; +ASSERT (-26 * x0) + (11 * x1) + (23 * x2) + (-5 * x3) >= 20 ; +ASSERT (7 * x0) + (28 * x1) + (6 * x2) + (-20 * x3) <= -16 ; +ASSERT (-15 * x0) + (21 * x1) + (5 * x2) + (-2 * x3) <= 11 ; +ASSERT (-5 * x0) + (-16 * x1) + (-16 * x2) + (14 * x3) <= 12 ; +ASSERT (3 * x0) + (28 * x1) + (22 * x2) + (-6 * x3) >= -31 ; +ASSERT (15 * x0) + (-13 * x1) + (10 * x2) + (21 * x3) <= -25 ; +ASSERT (1 * x0) + (-24 * x1) + (-30 * x2) + (25 * x3) > 17 ; +ASSERT (12 * x0) + (-3 * x1) + (0 * x2) + (23 * x3) < -12 ; +ASSERT (16 * x0) + (-9 * x1) + (1 * x2) + (-15 * x3) < -6; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-089.cvc b/test/regress/regress1/arith/arith-int-089.cvc new file mode 100644 index 000000000..7ff36d29e --- /dev/null +++ b/test/regress/regress1/arith/arith-int-089.cvc @@ -0,0 +1,13 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (14 * x0) + (-14 * x1) + (-29 * x2) + (31 * x3) = -15 ; +ASSERT (-14 * x0) + (2 * x1) + (26 * x2) + (29 * x3) = 25 ; +ASSERT (19 * x0) + (-7 * x1) + (-15 * x2) + (12 * x3) = 32 ; +ASSERT (5 * x0) + (32 * x1) + (22 * x2) + (1 * x3) = -13 ; +ASSERT (-12 * x0) + (-9 * x1) + (-30 * x2) + (-13 * x3) >= 0 ; +ASSERT (-9 * x0) + (7 * x1) + (-24 * x2) + (22 * x3) >= 11 ; +ASSERT (28 * x0) + (-5 * x1) + (12 * x2) + (15 * x3) >= 31 ; +ASSERT (5 * x0) + (-6 * x1) + (5 * x2) + (-2 * x3) >= -5 ; +ASSERT (-14 * x0) + (-17 * x1) + (-29 * x2) + (-8 * x3) < -32 ; +ASSERT (20 * x0) + (-19 * x1) + (-27 * x2) + (-20 * x3) >= -2; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-090.cvc b/test/regress/regress1/arith/arith-int-090.cvc new file mode 100644 index 000000000..52b9c13f0 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-090.cvc @@ -0,0 +1,13 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-13 * x0) + (-14 * x1) + (-10 * x2) + (32 * x3) = 11 ; +ASSERT (28 * x0) + (21 * x1) + (-20 * x2) + (-32 * x3) > -31 ; +ASSERT (10 * x0) + (19 * x1) + (-10 * x2) + (-2 * x3) > -31 ; +ASSERT (-31 * x0) + (17 * x1) + (15 * x2) + (31 * x3) > -12 ; +ASSERT (-17 * x0) + (16 * x1) + (17 * x2) + (-11 * x3) >= 17 ; +ASSERT (19 * x0) + (-31 * x1) + (-16 * x2) + (-29 * x3) >= 15 ; +ASSERT (24 * x0) + (-32 * x1) + (27 * x2) + (11 * x3) < 26 ; +ASSERT (-2 * x0) + (5 * x1) + (-21 * x2) + (24 * x3) >= -17 ; +ASSERT (13 * x0) + (11 * x1) + (-28 * x2) + (-5 * x3) > 16 ; +ASSERT (-16 * x0) + (17 * x1) + (22 * x2) + (6 * x3) > 21; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-091.cvc b/test/regress/regress1/arith/arith-int-091.cvc new file mode 100644 index 000000000..29a19db39 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-091.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (26 * x0) + (32 * x1) + (-26 * x2) + (-26 * x3) = -26 ; +ASSERT (30 * x0) + (17 * x1) + (28 * x2) + (-9 * x3) = -21 ; +ASSERT (15 * x0) + (9 * x1) + (-13 * x2) + (-21 * x3) = -13 ; +ASSERT (-4 * x0) + (16 * x1) + (-5 * x2) + (8 * x3) = -25 ; +ASSERT (-11 * x0) + (26 * x1) + (1 * x2) + (23 * x3) < 6 ; +ASSERT (-31 * x0) + (-25 * x1) + (1 * x2) + (16 * x3) > -8 ; +ASSERT (9 * x0) + (-19 * x1) + (28 * x2) + (15 * x3) < -30 ; +ASSERT (32 * x0) + (18 * x1) + (2 * x2) + (31 * x3) > -7 ; +ASSERT (24 * x0) + (29 * x1) + (20 * x2) + (-16 * x3) >= 3 ; +ASSERT (-1 * x0) + (17 * x1) + (-27 * x2) + (-32 * x3) >= 20 ; +ASSERT (26 * x0) + (-23 * x1) + (6 * x2) + (30 * x3) <= 5 ; +ASSERT (13 * x0) + (6 * x1) + (-26 * x2) + (1 * x3) > -29 ; +ASSERT (26 * x0) + (2 * x1) + (8 * x2) + (-18 * x3) <= 32 ; +ASSERT (-21 * x0) + (28 * x1) + (23 * x2) + (4 * x3) <= -31 ; +ASSERT (26 * x0) + (2 * x1) + (-28 * x2) + (12 * x3) > 6 ; +ASSERT (-20 * x0) + (-22 * x1) + (-16 * x2) + (-21 * x3) <= -1 ; +ASSERT (21 * x0) + (-22 * x1) + (19 * x2) + (32 * x3) <= -10 ; +ASSERT (3 * x0) + (28 * x1) + (-11 * x2) + (0 * x3) > 0 ; +ASSERT (-13 * x0) + (-16 * x1) + (-17 * x2) + (-2 * x3) <= -17; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-092.cvc b/test/regress/regress1/arith/arith-int-092.cvc new file mode 100644 index 000000000..51c8a6bc4 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-092.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-20 * x0) + (19 * x1) + (16 * x2) + (-27 * x3) = -22 ; +ASSERT (12 * x0) + (-18 * x1) + (-25 * x2) + (-1 * x3) = -22 ; +ASSERT (17 * x0) + (11 * x1) + (24 * x2) + (16 * x3) = -3 ; +ASSERT (15 * x0) + (-10 * x1) + (-15 * x2) + (25 * x3) = -30 ; +ASSERT (7 * x0) + (26 * x1) + (-8 * x2) + (-29 * x3) >= -32 ; +ASSERT (20 * x0) + (25 * x1) + (-23 * x2) + (13 * x3) >= -30 ; +ASSERT (27 * x0) + (-32 * x1) + (-27 * x2) + (13 * x3) >= -12 ; +ASSERT (25 * x0) + (-16 * x1) + (32 * x2) + (-6 * x3) >= -30 ; +ASSERT (32 * x0) + (-18 * x1) + (-6 * x2) + (-32 * x3) <= -26 ; +ASSERT (25 * x0) + (12 * x1) + (25 * x2) + (-14 * x3) > 5 ; +ASSERT (-4 * x0) + (-20 * x1) + (12 * x2) + (-30 * x3) >= 13 ; +ASSERT (8 * x0) + (18 * x1) + (0 * x2) + (-28 * x3) <= 18 ; +ASSERT (-32 * x0) + (-25 * x1) + (23 * x2) + (5 * x3) < 29 ; +ASSERT (7 * x0) + (19 * x1) + (2 * x2) + (-31 * x3) > 7 ; +ASSERT (24 * x0) + (-17 * x1) + (-31 * x2) + (31 * x3) > 0 ; +ASSERT (13 * x0) + (20 * x1) + (-1 * x2) + (17 * x3) > 1 ; +ASSERT (17 * x0) + (26 * x1) + (6 * x2) + (29 * x3) >= -10 ; +ASSERT (-25 * x0) + (4 * x1) + (-22 * x2) + (14 * x3) < -23 ; +ASSERT (24 * x0) + (2 * x1) + (4 * x2) + (2 * x3) < 1; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-093.cvc b/test/regress/regress1/arith/arith-int-093.cvc new file mode 100644 index 000000000..7d2123d41 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-093.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (22 * x0) + (-2 * x1) + (-1 * x2) + (-24 * x3) = 8 ; +ASSERT (-6 * x0) + (9 * x1) + (-20 * x2) + (-23 * x3) = 14 ; +ASSERT (-11 * x0) + (4 * x1) + (24 * x2) + (-6 * x3) <= -23 ; +ASSERT (3 * x0) + (5 * x1) + (-5 * x2) + (17 * x3) < -17 ; +ASSERT (-10 * x0) + (-20 * x1) + (-16 * x2) + (-29 * x3) >= 6 ; +ASSERT (-28 * x0) + (1 * x1) + (-22 * x2) + (-16 * x3) >= 4 ; +ASSERT (19 * x0) + (8 * x1) + (-8 * x2) + (-2 * x3) > -23 ; +ASSERT (11 * x0) + (17 * x1) + (30 * x2) + (31 * x3) < -32 ; +ASSERT (23 * x0) + (30 * x1) + (-12 * x2) + (16 * x3) <= 4 ; +ASSERT (-23 * x0) + (-8 * x1) + (21 * x2) + (21 * x3) <= -14 ; +ASSERT (13 * x0) + (15 * x1) + (-6 * x2) + (-1 * x3) >= -8 ; +ASSERT (-21 * x0) + (18 * x1) + (27 * x2) + (-16 * x3) <= 11 ; +ASSERT (30 * x0) + (-6 * x1) + (5 * x2) + (-27 * x3) <= -7 ; +ASSERT (0 * x0) + (3 * x1) + (13 * x2) + (28 * x3) > -21 ; +ASSERT (-15 * x0) + (-20 * x1) + (10 * x2) + (-23 * x3) < 27 ; +ASSERT (24 * x0) + (6 * x1) + (-29 * x2) + (1 * x3) <= -23 ; +ASSERT (-24 * x0) + (-14 * x1) + (-15 * x2) + (8 * x3) > -19 ; +ASSERT (17 * x0) + (15 * x1) + (8 * x2) + (-31 * x3) >= -16 ; +ASSERT (-19 * x0) + (7 * x1) + (-28 * x2) + (20 * x3) < -19; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-094.cvc b/test/regress/regress1/arith/arith-int-094.cvc new file mode 100644 index 000000000..a5f1aefce --- /dev/null +++ b/test/regress/regress1/arith/arith-int-094.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (-7 * x0) + (-11 * x1) + (26 * x2) + (10 * x3) = 31 ; +ASSERT (-17 * x0) + (-20 * x1) + (24 * x2) + (-9 * x3) = -32 ; +ASSERT (5 * x0) + (14 * x1) + (7 * x2) + (-29 * x3) = 31 ; +ASSERT (17 * x0) + (8 * x1) + (23 * x2) + (-26 * x3) <= -12 ; +ASSERT (7 * x0) + (29 * x1) + (24 * x2) + (4 * x3) <= -21 ; +ASSERT (-16 * x0) + (7 * x1) + (7 * x2) + (-29 * x3) < -16 ; +ASSERT (-7 * x0) + (-11 * x1) + (-17 * x2) + (22 * x3) > -11 ; +ASSERT (-10 * x0) + (-17 * x1) + (21 * x2) + (29 * x3) > -7 ; +ASSERT (-28 * x0) + (-26 * x1) + (-24 * x2) + (-21 * x3) < -20 ; +ASSERT (-32 * x0) + (26 * x1) + (-8 * x2) + (2 * x3) >= -18 ; +ASSERT (18 * x0) + (-23 * x1) + (-26 * x2) + (-24 * x3) > -30 ; +ASSERT (-9 * x0) + (31 * x1) + (-26 * x2) + (-22 * x3) < -15 ; +ASSERT (27 * x0) + (-1 * x1) + (10 * x2) + (28 * x3) < -20 ; +ASSERT (-4 * x0) + (-22 * x1) + (-24 * x2) + (2 * x3) < -13 ; +ASSERT (-4 * x0) + (-23 * x1) + (-16 * x2) + (18 * x3) > -20 ; +ASSERT (13 * x0) + (-30 * x1) + (-3 * x2) + (-25 * x3) <= 31 ; +ASSERT (21 * x0) + (-28 * x1) + (22 * x2) + (19 * x3) > 7 ; +ASSERT (-2 * x0) + (-31 * x1) + (24 * x2) + (18 * x3) > 27 ; +ASSERT (-14 * x0) + (-5 * x1) + (-22 * x2) + (1 * x3) <= -15; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-095.cvc b/test/regress/regress1/arith/arith-int-095.cvc new file mode 100644 index 000000000..bc47d6f49 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-095.cvc @@ -0,0 +1,22 @@ +% EXPECT: valid +x0, x1, x2, x3 : INT; +ASSERT (2 * x0) + (28 * x1) + (3 * x2) + (8 * x3) > -32 ; +ASSERT (-15 * x0) + (21 * x1) + (-11 * x2) + (28 * x3) <= -19 ; +ASSERT (32 * x0) + (29 * x1) + (-1 * x2) + (-10 * x3) < -23 ; +ASSERT (6 * x0) + (-27 * x1) + (29 * x2) + (28 * x3) < 5 ; +ASSERT (-7 * x0) + (-7 * x1) + (-28 * x2) + (32 * x3) <= -32 ; +ASSERT (-10 * x0) + (20 * x1) + (-28 * x2) + (-28 * x3) >= -6 ; +ASSERT (-13 * x0) + (-9 * x1) + (4 * x2) + (-32 * x3) > -1 ; +ASSERT (-21 * x0) + (4 * x1) + (0 * x2) + (-13 * x3) >= -1 ; +ASSERT (18 * x0) + (-21 * x1) + (-16 * x2) + (24 * x3) <= -12 ; +ASSERT (18 * x0) + (-10 * x1) + (-10 * x2) + (-3 * x3) <= -10 ; +ASSERT (-32 * x0) + (9 * x1) + (-24 * x2) + (-19 * x3) < -4 ; +ASSERT (12 * x0) + (20 * x1) + (31 * x2) + (-25 * x3) <= 23 ; +ASSERT (-22 * x0) + (15 * x1) + (-12 * x2) + (-6 * x3) < 18 ; +ASSERT (-25 * x0) + (-8 * x1) + (32 * x2) + (26 * x3) > -20 ; +ASSERT (-30 * x0) + (27 * x1) + (0 * x2) + (27 * x3) >= 7 ; +ASSERT (-8 * x0) + (-2 * x1) + (-6 * x2) + (-21 * x3) <= 21 ; +ASSERT (8 * x0) + (-31 * x1) + (-4 * x2) + (1 * x3) > -11 ; +ASSERT (22 * x0) + (-25 * x1) + (-26 * x2) + (10 * x3) < -32 ; +ASSERT (-12 * x0) + (-13 * x1) + (15 * x2) + (4 * x3) < 26; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-096.cvc b/test/regress/regress1/arith/arith-int-096.cvc new file mode 100644 index 000000000..2f6cf3155 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-096.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (23 * x0) + (24 * x1) + (19 * x2) + (-3 * x3) = -16 ; +ASSERT (2 * x0) + (-13 * x1) + (5 * x2) + (-1 * x3) = 28; +ASSERT (-6 * x0) + (-5 * x1) + (-2 * x2) + (-9 * x3) > -3 ; +ASSERT (30 * x0) + (22 * x1) + (-20 * x2) + (1 * x3) > -12 ; +ASSERT (-8 * x0) + (-25 * x1) + (28 * x2) + (-25 * x3) <= -8 ; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-097.cvc b/test/regress/regress1/arith/arith-int-097.cvc new file mode 100644 index 000000000..b05061192 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-097.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (19 * x0) + (-11 * x1) + (-19 * x2) + (5 * x3) = 26 ; +ASSERT (1 * x0) + (-28 * x1) + (-2 * x2) + (15 * x3) < 9 ; +ASSERT (-8 * x0) + (-1 * x1) + (-25 * x2) + (-7 * x3) <= -31 ; +ASSERT (-7 * x0) + (11 * x1) + (-5 * x2) + (-19 * x3) > 32 ; +ASSERT (-22 * x0) + (13 * x1) + (-16 * x2) + (-12 * x3) <= 32; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-099.cvc b/test/regress/regress1/arith/arith-int-099.cvc new file mode 100644 index 000000000..0d74dcb39 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-099.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (-31 * x0) + (-20 * x1) + (-30 * x2) + (-28 * x3) = -24 ; +ASSERT (11 * x0) + (-32 * x1) + (-2 * x2) + (8 * x3) <= 16 ; +ASSERT (-10 * x0) + (16 * x1) + (31 * x2) + (19 * x3) >= -21 ; +ASSERT (-15 * x0) + (18 * x1) + (-16 * x2) + (7 * x3) <= -12 ; +ASSERT (14 * x0) + (-1 * x1) + (12 * x2) + (27 * x3) >= -12; +QUERY FALSE; diff --git a/test/regress/regress1/arith/arith-int-100.cvc b/test/regress/regress1/arith/arith-int-100.cvc new file mode 100644 index 000000000..7e07bee14 --- /dev/null +++ b/test/regress/regress1/arith/arith-int-100.cvc @@ -0,0 +1,8 @@ +% EXPECT: invalid +x0, x1, x2, x3 : INT; +ASSERT (27 * x0) + (-21 * x1) + (-6 * x2) + (-6 * x3) > -15 ; +ASSERT (-5 * x0) + (-10 * x1) + (2 * x2) + (-16 * x3) <= -7 ; +ASSERT (25 * x0) + (25 * x1) + (-15 * x2) + (-32 * x3) > -31 ; +ASSERT (17 * x0) + (-26 * x1) + (9 * x2) + (-28 * x3) >= -29 ; +ASSERT (-10 * x0) + (-18 * x1) + (15 * x2) + (0 * x3) <= 32; +QUERY FALSE; diff --git a/test/regress/regress1/arith/bug547.1.smt2 b/test/regress/regress1/arith/bug547.1.smt2 new file mode 100644 index 000000000..4b7cf9780 --- /dev/null +++ b/test/regress/regress1/arith/bug547.1.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --rewrite-divk +; EXPECT: unknown +(set-logic QF_NIA) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (= 1 (mod (* x y) 3))) +(check-sat) +(exit) diff --git a/test/regress/regress1/arith/bug716.0.smt2 b/test/regress/regress1/arith/bug716.0.smt2 new file mode 100644 index 000000000..2046f4911 --- /dev/null +++ b/test/regress/regress1/arith/bug716.0.smt2 @@ -0,0 +1,662 @@ +; COMMAND-LINE: --lang=smt2.5 +; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' -e 's/in a linear logic: .*$/in a linear logic: TERM/' +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. +; EXPECT: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 +(set-logic AUFBVDTLIRA) +;; produced by cvc4_15.drv ;; +(set-info :source |VC generated by SPARK 2014|) +(set-info :smt-lib-version 2.0) +(set-info :category industrial) +(set-info :status unknown) +;;; generated by SMT-LIB2 driver +;;; SMT-LIB2 driver: bit-vectors, common part +(set-option :produce-models true) +;;; SMT-LIB2: integer arithmetic +;;; SMT-LIB2: real arithmetic +(declare-datatypes () ((tuple0 (Tuple0)))) +(declare-sort us_private 0) + +(declare-fun us_null_ext__ () us_private) + +(declare-sort us_type_of_heap 0) + +(declare-datatypes () +((us_type_of_heap__ref + (mk___type_of_heap__ref (us_type_of_heap__content us_type_of_heap))))) +(declare-sort us_image 0) + +(declare-datatypes () ((int__ref (mk_int__ref (int__content Int))))) +(declare-datatypes () ((bool__ref (mk_bool__ref (bool__content Bool))))) +(declare-datatypes () ((real__ref (mk_real__ref (real__content Real))))) +(declare-datatypes () +((us_private__ref (mk___private__ref (us_private__content us_private))))) +(define-fun int__ref___projection ((a int__ref)) Int (int__content a)) + +(define-fun bool__ref___projection ((a bool__ref)) Bool (bool__content a)) + +(define-fun real__ref___projection ((a real__ref)) Real (real__content a)) + +(define-fun us_private__ref___projection ((a us_private__ref)) us_private + (us_private__content a)) + +(declare-fun us_compatible_tags (Int Int) Bool) + +;; __compatible_tags_refl + (assert (forall ((tag Int)) (us_compatible_tags tag tag))) + +(define-fun to_int1 ((b Bool)) Int (ite (= b true) 1 0)) + +(define-fun of_int ((i Int)) Bool (ite (= i 0) false true)) + +(define-fun in_range ((x Int)) Bool (or (= x 0) (= x 1))) + +(declare-fun attr__ATTRIBUTE_IMAGE (Bool) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE (us_image) Bool) + +(declare-fun power (Real Int) Real) + +;; Power_0 + (assert (forall ((x Real)) (= (power x 0) 1.0))) + +;; Power_s + (assert + (forall ((x Real) (n Int)) + (=> (<= 0 n) (= (power x (+ n 1)) (* x (power x n)))))) + +;; Power_s_alt + (assert + (forall ((x Real) (n Int)) + (=> (< 0 n) (= (power x n) (* x (power x (- n 1))))))) + +;; Power_1 + (assert (forall ((x Real)) (= (power x 1) x))) + +;; Power_sum + (assert + (forall ((x Real) (n Int) (m Int)) + (=> (<= 0 n) + (=> (<= 0 m) (= (power x (+ n m)) (* (power x n) (power x m))))))) + +;; Power_mult + (assert + (forall ((x Real) (n Int) (m Int)) + (=> (<= 0 n) (=> (<= 0 m) (= (power x (* n m)) (power (power x n) m)))))) + +;; Power_mult2 + (assert + (forall ((x Real) (y Real) (n Int)) + (=> (<= 0 n) (= (power (* x y) n) (* (power x n) (power y n)))))) + +;; Pow_ge_one + (assert + (forall ((x Real) (n Int)) + (=> (and (<= 0 n) (<= 1.0 x)) (<= 1.0 (power x n))))) + +(declare-datatypes () +((mode (NearestTiesToEven) (ToZero) (Up) (Down) (NearestTiesToAway)))) +(declare-sort single 0) + +(declare-fun round (mode Real) Real) + +(declare-fun value (single) Real) + +(declare-fun exact (single) Real) + +(declare-fun model (single) Real) + +(define-fun round_error ((x single)) Real (ite (>= (- (value x) (exact x)) 0.0) (- + (value x) (exact x)) (- (- (value x) (exact x))))) + +(define-fun total_error ((x single)) Real (ite (>= (- (value x) (model x)) 0.0) (- + (value x) (model x)) (- (- (value x) (model x))))) + +(define-fun no_overflow ((m mode) + (x Real)) Bool (<= (ite (>= (round m x) 0.0) (round m x) (- (round m x))) 340282346638528859811704183484516925440.0)) + +;; Bounded_real_no_overflow + (assert + (forall ((m mode) (x Real)) + (=> (<= (ite (>= x 0.0) x (- x)) 340282346638528859811704183484516925440.0) + (no_overflow m x)))) + +;; Round_monotonic + (assert + (forall ((m mode) (x Real) (y Real)) + (=> (<= x y) (<= (round m x) (round m y))))) + +;; Round_idempotent + (assert + (forall ((m1 mode) (m2 mode) (x Real)) + (= (round m1 (round m2 x)) (round m2 x)))) + +;; Round_value + (assert (forall ((m mode) (x single)) (= (round m (value x)) (value x)))) + +;; Bounded_value + (assert + (forall ((x single)) + (<= (ite (>= (value x) 0.0) (value x) (- (value x))) 340282346638528859811704183484516925440.0))) + +;; Exact_rounding_for_integers + (assert + (forall ((m mode) (i Int)) + (=> (and (<= (- 16777216) i) (<= i 16777216)) + (= (round m (to_real i)) (to_real i))))) + +;; Round_down_le + (assert (forall ((x Real)) (<= (round Down x) x))) + +;; Round_up_ge + (assert (forall ((x Real)) (<= x (round Up x)))) + +;; Round_down_neg + (assert (forall ((x Real)) (= (round Down (- x)) (- (round Up x))))) + +;; Round_up_neg + (assert (forall ((x Real)) (= (round Up (- x)) (- (round Down x))))) + +(declare-fun round_logic (mode Real) single) + +;; Round_logic_def + (assert + (forall ((m mode) (x Real)) + (=> (no_overflow m x) (= (value (round_logic m x)) (round m x))))) + +(define-fun of_real_post ((m mode) (x Real) + (res single)) Bool (and (= (value res) (round m x)) + (and (= (exact res) x) (= (model res) x)))) + +(define-fun add_post ((m mode) (x single) (y single) + (res single)) Bool (and (= (value res) (round m (+ (value x) (value y)))) + (and (= (exact res) (+ (exact x) (exact y))) + (= (model res) (+ (model x) (model y)))))) + +(define-fun sub_post ((m mode) (x single) (y single) + (res single)) Bool (and (= (value res) (round m (- (value x) (value y)))) + (and (= (exact res) (- (exact x) (exact y))) + (= (model res) (- (model x) (model y)))))) + +(define-fun mul_post ((m mode) (x single) (y single) + (res single)) Bool (and (= (value res) (round m (* (value x) (value y)))) + (and (= (exact res) (* (exact x) (exact y))) + (= (model res) (* (model x) (model y)))))) + +(define-fun div_post ((m mode) (x single) (y single) + (res single)) Bool (and (= (value res) (round m (/ (value x) (value y)))) + (and (= (exact res) (/ (exact x) (exact y))) + (= (model res) (/ (model x) (model y)))))) + +(define-fun neg_post ((x single) + (res single)) Bool (and (= (value res) (- (value x))) + (and (= (exact res) (- (exact x))) + (= (model res) (- (model x)))))) + +(define-fun lt ((x single) (y single)) Bool (< (value x) (value y))) + +(define-fun gt ((x single) (y single)) Bool (< (value y) (value x))) + +(declare-sort double 0) + +(declare-fun round1 (mode Real) Real) + +(declare-fun value1 (double) Real) + +(declare-fun exact1 (double) Real) + +(declare-fun model1 (double) Real) + +(define-fun round_error1 ((x double)) Real (ite (>= (- (value1 x) (exact1 x)) 0.0) (- + (value1 x) (exact1 x)) (- (- (value1 x) (exact1 x))))) + +(define-fun total_error1 ((x double)) Real (ite (>= (- (value1 x) (model1 x)) 0.0) (- + (value1 x) (model1 x)) (- (- (value1 x) (model1 x))))) + +(define-fun no_overflow1 ((m mode) + (x Real)) Bool (<= (ite (>= (round1 m x) 0.0) (round1 m x) (- (round1 m x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0)) + +;; Bounded_real_no_overflow + (assert + (forall ((m mode) (x Real)) + (=> + (<= (ite (>= x 0.0) x (- x)) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0) + (no_overflow1 m x)))) + +;; Round_monotonic + (assert + (forall ((m mode) (x Real) (y Real)) + (=> (<= x y) (<= (round1 m x) (round1 m y))))) + +;; Round_idempotent + (assert + (forall ((m1 mode) (m2 mode) (x Real)) + (= (round1 m1 (round1 m2 x)) (round1 m2 x)))) + +;; Round_value + (assert + (forall ((m mode) (x double)) (= (round1 m (value1 x)) (value1 x)))) + +;; Bounded_value + (assert + (forall ((x double)) + (<= (ite (>= (value1 x) 0.0) (value1 x) (- (value1 x))) 179769313486231570814527423731704356798070567525844996598917476803157260780028538760589558632766878171540458953514382464234321326889464182768467546703537516986049910576551282076245490090389328944075868508455133942304583236903222948165808559332123348274797826204144723168738177180919299881250404026184124858368.0))) + +;; Exact_rounding_for_integers + (assert + (forall ((m mode) (i Int)) + (=> (and (<= (- 9007199254740992) i) (<= i 9007199254740992)) + (= (round1 m (to_real i)) (to_real i))))) + +;; Round_down_le + (assert (forall ((x Real)) (<= (round1 Down x) x))) + +;; Round_up_ge + (assert (forall ((x Real)) (<= x (round1 Up x)))) + +;; Round_down_neg + (assert (forall ((x Real)) (= (round1 Down (- x)) (- (round1 Up x))))) + +;; Round_up_neg + (assert (forall ((x Real)) (= (round1 Up (- x)) (- (round1 Down x))))) + +(declare-fun round_logic1 (mode Real) double) + +;; Round_logic_def + (assert + (forall ((m mode) (x Real)) + (=> (no_overflow1 m x) (= (value1 (round_logic1 m x)) (round1 m x))))) + +(define-fun of_real_post1 ((m mode) (x Real) + (res double)) Bool (and (= (value1 res) (round1 m x)) + (and (= (exact1 res) x) (= (model1 res) x)))) + +(define-fun add_post1 ((m mode) (x double) (y double) + (res double)) Bool (and + (= (value1 res) (round1 m (+ (value1 x) (value1 y)))) + (and (= (exact1 res) (+ (exact1 x) (exact1 y))) + (= (model1 res) (+ (model1 x) (model1 y)))))) + +(define-fun sub_post1 ((m mode) (x double) (y double) + (res double)) Bool (and + (= (value1 res) (round1 m (- (value1 x) (value1 y)))) + (and (= (exact1 res) (- (exact1 x) (exact1 y))) + (= (model1 res) (- (model1 x) (model1 y)))))) + +(define-fun mul_post1 ((m mode) (x double) (y double) + (res double)) Bool (and + (= (value1 res) (round1 m (* (value1 x) (value1 y)))) + (and (= (exact1 res) (* (exact1 x) (exact1 y))) + (= (model1 res) (* (model1 x) (model1 y)))))) + +(define-fun div_post1 ((m mode) (x double) (y double) + (res double)) Bool (and + (= (value1 res) (round1 m (/ (value1 x) (value1 y)))) + (and (= (exact1 res) (/ (exact1 x) (exact1 y))) + (= (model1 res) (/ (model1 x) (model1 y)))))) + +(define-fun neg_post1 ((x double) + (res double)) Bool (and (= (value1 res) (- (value1 x))) + (and (= (exact1 res) (- (exact1 x))) + (= (model1 res) (- (model1 x)))))) + +(define-fun lt1 ((x double) (y double)) Bool (< (value1 x) (value1 y))) + +(define-fun gt1 ((x double) (y double)) Bool (< (value1 y) (value1 x))) + +;; round_single_bound + (assert + (forall ((x Real)) + (! (and + (<= (- (- x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)) + (round NearestTiesToEven x)) + (<= (round NearestTiesToEven x) (+ (+ x (* (/ 1.0 16777216.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 1427247692705959881058285969449495136382746624.0)))) :pattern ( + (round NearestTiesToEven x)) ))) + +;; round_double_bound + (assert + (forall ((x Real)) + (! (and + (<= (- (- x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)) + (round1 NearestTiesToEven x)) + (<= (round1 NearestTiesToEven x) (+ (+ x (* (/ 1.0 9007199254740992.0) (ite (>= x 0.0) x (- x)))) (/ 1.0 404804506614621236704990693437834614099113299528284236713802716054860679135990693783920767402874248990374155728633623822779617474771586953734026799881477019843034848553132722728933815484186432682479535356945490137124014966849385397236206711298319112681620113024717539104666829230461005064372655017292012526615415482186989568.0)))) :pattern ( + (round1 NearestTiesToEven x)) ))) + +;; round_double_single + (assert + (forall ((x Real)) + (! (= (round1 NearestTiesToEven (round NearestTiesToEven x)) (round + NearestTiesToEven + x)) :pattern ( + (round NearestTiesToEven x)) ))) + +(declare-fun round2 (Real) Int) + +;; Round_down + (assert + (forall ((x Real)) + (=> (< (- x (to_real (to_int x))) (/ 5.0 10.0)) (= (round2 x) (to_int x))))) + +;; Round_up + (assert + (forall ((x Real)) + (=> (< (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0)) + (= (round2 x) (- 1 (to_int (- 1.0 x))))))) + +;; Round_neg_tie + (assert + (forall ((x Real)) + (=> (and (= (- x (to_real (to_int x))) (/ 5.0 10.0)) (< x 0.0)) + (= (round2 x) (to_int x))))) + +;; Round_pos_tie + (assert + (forall ((x Real)) + (=> + (and (= (- (to_real (- 1 (to_int (- 1.0 x)))) x) (/ 5.0 10.0)) (< 0.0 x)) + (= (round2 x) (- 1 (to_int (- 1.0 x))))))) + +;; Round_int + (assert + (forall ((i Int)) + (! (= (round2 (to_real i)) i) :pattern ((round2 (to_real i))) ))) + +;; Round_near_int + (assert + (forall ((i Int)) + (forall ((x Real)) + (=> (and (< (- (/ 5.0 10.0)) x) (< x (/ 5.0 10.0))) + (= (round2 (+ (to_real i) x)) i))))) + +;; Round_monotonic + (assert + (forall ((x Real) (y Real)) (=> (<= x y) (<= (round2 x) (round2 y))))) + +;; Round_monotonic_int1 + (assert + (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (round2 x) i)))) + +;; Round_monotonic_int2 + (assert + (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (round2 x))))) + +;; Round_bound + (assert + (forall ((x Real)) + (and (<= (- x (/ 5.0 10.0)) (to_real (round2 x))) + (<= (to_real (round2 x)) (+ x (/ 5.0 10.0)))))) + +(declare-fun remainder (Real Real) Real) + +(declare-sort float 0) + +(define-fun in_range1 ((x Real)) Bool (and + (<= (- 340282346638528859811704183484516925440.0) x) + (<= x 340282346638528859811704183484516925440.0))) + +(declare-fun to_real1 (float) Real) + +(declare-fun of_real (Real) float) + +(declare-fun user_eq (float float) Bool) + +(declare-fun next_representable (Real) Real) + +(declare-fun prev_representable (Real) Real) + +;; next_representable_def + (assert + (forall ((x Real)) + (! (< x (next_representable x)) :pattern ((next_representable x)) ))) + +;; prev_representable_def + (assert + (forall ((x Real)) + (! (< (prev_representable x) x) :pattern ((prev_representable x)) ))) + +(declare-fun attr__ATTRIBUTE_IMAGE1 (Real) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check1 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE1 (us_image) Real) + +(declare-fun dummy () float) + +;; inversion_axiom + (assert + (forall ((x float)) + (! (= (of_real (to_real1 x)) x) :pattern ((to_real1 x)) ))) + +;; representable_first + (assert + (= (round NearestTiesToEven (- 340282346638528859811704183484516925440.0)) (- 340282346638528859811704183484516925440.0))) + +;; representable_last + (assert + (= (round NearestTiesToEven 340282346638528859811704183484516925440.0) 340282346638528859811704183484516925440.0)) + +;; range_axiom + (assert (forall ((x float)) (in_range1 (to_real1 x)))) + +(declare-datatypes () ((float__ref (mk_float__ref (float__content float))))) +(define-fun float__ref___projection ((a float__ref)) float (float__content a)) + +(declare-sort weapon_kind 0) + +(define-fun in_range2 ((x Int)) Bool (and (<= 0 x) (<= x 2))) + +(define-fun bool_eq ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE2 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check2 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE2 (us_image) Int) + +(declare-fun to_rep (weapon_kind) Int) + +(declare-fun of_rep (Int) weapon_kind) + +(declare-fun user_eq1 (weapon_kind weapon_kind) Bool) + +(declare-fun dummy1 () weapon_kind) + +;; inversion_axiom + (assert + (forall ((x weapon_kind)) + (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) ))) + +;; range_axiom + (assert + (forall ((x weapon_kind)) (! (in_range2 + (to_rep x)) :pattern ((to_rep x)) ))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range2 x) (= (to_rep (of_rep x)) x)) :pattern ((to_rep + (of_rep x))) ))) + +(declare-datatypes () +((weapon_kind__ref (mk_weapon_kind__ref (weapon_kind__content weapon_kind))))) +(define-fun weapon_kind__ref___projection ((a weapon_kind__ref)) weapon_kind + (weapon_kind__content a)) + +(declare-fun dps (Int) float) + +(declare-fun damage (Int) Int) + +(declare-fun bullet (Int) Int) + +(declare-fun cooldown (Int) Int) + +;; dps__post_axiom + (assert true) + +;; dps__def_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) + (= (to_real1 (dps self)) (round NearestTiesToEven + (/ (round NearestTiesToEven + (to_real (damage (bullet self)))) (round + NearestTiesToEven + (to_real + (cooldown + self))))))) :pattern ( + (dps self)) ))) + +(declare-sort integer 0) + +(define-fun in_range3 ((x Int)) Bool (and (<= (- 2147483648) x) + (<= x 2147483647))) + +(define-fun bool_eq1 ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE3 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check3 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE3 (us_image) Int) + +(declare-fun to_rep1 (integer) Int) + +(declare-fun of_rep1 (Int) integer) + +(declare-fun user_eq2 (integer integer) Bool) + +(declare-fun dummy2 () integer) + +;; inversion_axiom + (assert + (forall ((x integer)) + (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) ))) + +;; range_axiom + (assert + (forall ((x integer)) (! (in_range3 (to_rep1 x)) :pattern ((to_rep1 x)) ))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range3 x) (= (to_rep1 (of_rep1 x)) x)) :pattern ((to_rep1 + (of_rep1 x))) ))) + +(declare-datatypes () +((integer__ref (mk_integer__ref (integer__content integer))))) +(define-fun integer__ref___projection ((a integer__ref)) integer (integer__content + a)) + +(define-fun dynamic_invariant ((temp___expr_15 Int) (temp___is_init_12 Bool) + (temp___do_constant_13 Bool) + (temp___do_toplevel_14 Bool)) Bool (=> + (or (= temp___is_init_12 true) + (<= (- 2147483648) 2147483647)) + (in_range3 temp___expr_15))) + +(declare-sort bullet_kind 0) + +(define-fun in_range4 ((x Int)) Bool (and (<= 0 x) (<= x 4))) + +(define-fun bool_eq2 ((x Int) (y Int)) Bool (ite (= x y) true false)) + +(declare-fun attr__ATTRIBUTE_IMAGE4 (Int) us_image) + +(declare-fun attr__ATTRIBUTE_VALUE__pre_check4 (us_image) Bool) + +(declare-fun attr__ATTRIBUTE_VALUE4 (us_image) Int) + +(declare-fun to_rep2 (bullet_kind) Int) + +(declare-fun of_rep2 (Int) bullet_kind) + +(declare-fun user_eq3 (bullet_kind bullet_kind) Bool) + +(declare-fun dummy3 () bullet_kind) + +;; inversion_axiom + (assert + (forall ((x bullet_kind)) + (! (= (of_rep2 (to_rep2 x)) x) :pattern ((to_rep2 x)) ))) + +;; range_axiom + (assert + (forall ((x bullet_kind)) (! (in_range4 + (to_rep2 x)) :pattern ((to_rep2 x)) ))) + +;; coerce_axiom + (assert + (forall ((x Int)) + (! (=> (in_range4 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2 + (of_rep2 x))) ))) + +(declare-datatypes () +((bullet_kind__ref (mk_bullet_kind__ref (bullet_kind__content bullet_kind))))) +(define-fun bullet_kind__ref___projection ((a bullet_kind__ref)) bullet_kind + (bullet_kind__content a)) + +(define-fun dynamic_invariant1 ((temp___expr_180 Int) + (temp___is_init_177 Bool) (temp___do_constant_178 Bool) + (temp___do_toplevel_179 Bool)) Bool (=> + (or (= temp___is_init_177 true) + (<= 0 4)) (in_range4 temp___expr_180))) + +;; damage__post_axiom + (assert + (forall ((self Int)) + (! (=> (in_range4 self) (dynamic_invariant (damage self) true false true)) :pattern ( + (damage self)) ))) + +;; damage__def_axiom + (assert + (forall ((self Int)) + (! (=> (in_range4 self) + (= (damage self) (ite (= self 0) 0 + (ite (= self 1) 1 + (ite (= self 2) 8 (ite (= self 3) 10 1)))))) :pattern ( + (damage self)) ))) + +(define-fun dynamic_invariant2 ((temp___expr_186 Int) + (temp___is_init_183 Bool) (temp___do_constant_184 Bool) + (temp___do_toplevel_185 Bool)) Bool (=> + (or (= temp___is_init_183 true) + (<= 0 2)) (in_range2 temp___expr_186))) + +;; bullet__post_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) (dynamic_invariant1 (bullet self) true false true)) :pattern ( + (bullet self)) ))) + +;; bullet__def_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) + (= (bullet self) (ite (= self 0) 1 (ite (= self 1) 1 2)))) :pattern ( + (bullet self)) ))) + +;; cooldown__post_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) (dynamic_invariant (cooldown self) true false + true)) :pattern ((cooldown self)) ))) + +;; cooldown__def_axiom + (assert + (forall ((self Int)) + (! (=> (in_range2 self) + (= (cooldown self) (ite (= self 0) 4 (ite (= self 1) 1 8)))) :pattern ( + (cooldown self)) ))) + +(assert +;; WP_parameter_def + ;; File "weapons.ads", line 34, characters 0-0 + (not + (forall ((w Int)) + (=> (and (<= 0 w) (<= w 2)) + (or (= w 2) (<= (to_real1 (dps w)) (to_real1 (dps (+ w 1))))))))) +(check-sat) +(get-info :reason-unknown) diff --git a/test/regress/regress1/arith/bug716.1.cvc b/test/regress/regress1/arith/bug716.1.cvc new file mode 100644 index 000000000..d9330c727 --- /dev/null +++ b/test/regress/regress1/arith/bug716.1.cvc @@ -0,0 +1,6 @@ +% EXPECT: The POW(^) operator can only be used with a natural number in the exponent. Exception occurred in: +% EXPECT: 2 ^ x +% EXIT: 1 +x: INT; +ASSERT 2^x = 8; +QUERY x=3; diff --git a/test/regress/regress1/arith/div.03.smt2 b/test/regress/regress1/arith/div.03.smt2 new file mode 100644 index 000000000..8beef7a69 --- /dev/null +++ b/test/regress/regress1/arith/div.03.smt2 @@ -0,0 +1,12 @@ +; EXPECT: unsat +(set-logic QF_NIA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-fun x () Int) +(declare-fun n () Int) + +(assert (> n 0)) +(assert (>= x n)) +(assert (< (div x n) 1)) + +(check-sat) diff --git a/test/regress/regress1/arith/div.06.smt2 b/test/regress/regress1/arith/div.06.smt2 new file mode 100644 index 000000000..6e72433ac --- /dev/null +++ b/test/regress/regress1/arith/div.06.smt2 @@ -0,0 +1,14 @@ +; EXPECT: sat +(set-logic QF_NRA) +(set-info :smt-lib-version 2.0) +(set-info :status sat) +(declare-fun x () Real) +(declare-fun y () Real) +(declare-fun n () Real) + +(assert (= (/ x n) 0)) +(assert (= (/ y n) 1)) +(assert (<= n 0)) +(assert (>= n 0)) + +(check-sat) diff --git a/test/regress/regress1/arith/div.08.smt2 b/test/regress/regress1/arith/div.08.smt2 new file mode 100644 index 000000000..0b0d73ac1 --- /dev/null +++ b/test/regress/regress1/arith/div.08.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_NIA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-fun n () Int) + + +(assert (= (div n n) (div (div n n) n))) +(assert (distinct (div (div n n) n) (div (div (div n n) n) n))) +(assert (<= n 0)) +(assert (>= n 0)) +(check-sat) diff --git a/test/regress/regress1/arith/div.09.smt2 b/test/regress/regress1/arith/div.09.smt2 new file mode 100644 index 000000000..1c4bbde2b --- /dev/null +++ b/test/regress/regress1/arith/div.09.smt2 @@ -0,0 +1,14 @@ +; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/' +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. +; EXPECT: The fact in question: TERM +; EXPECT: ") +; EXIT: 1 +(set-logic QF_LRA) +(set-info :status unknown) +(declare-fun n () Real) + +; This example is test that LRA rejects multiplication terms + +(assert (= (/ n n) 1)) + +(check-sat) diff --git a/test/regress/regress1/arith/miplib3.cvc b/test/regress/regress1/arith/miplib3.cvc new file mode 100644 index 000000000..9e1ae5a62 --- /dev/null +++ b/test/regress/regress1/arith/miplib3.cvc @@ -0,0 +1,33 @@ +% COMMAND-LINE: --enable-miplib-trick +% EXPECT: sat + +tmp1, tmp2, tmp3, tmp4 : INT; +x, y, z : BOOLEAN; + +% x = {0, 1}, (NOT x) = 1 - x +% i*Nx + j*Ny + k = 0 +% i*x + j*Ny + k = 4 +% i*Nx + j*y + k = 6 +% i*x + j*y + k = 10 + +ASSERT NOT x AND (NOT y AND TRUE) => tmp1 = 0; +ASSERT x AND (NOT y AND TRUE) => tmp1 = 4; +ASSERT NOT x AND ( y AND TRUE) => tmp1 = 6; +ASSERT x AND ( y AND TRUE) => tmp1 = 10; + +ASSERT NOT x AND (NOT z AND TRUE) => tmp2 = 0; +ASSERT x AND (NOT z AND TRUE) => tmp2 = 2; +ASSERT NOT x AND ( z AND TRUE) => tmp2 = 9; +ASSERT x AND ( z AND TRUE) => tmp2 = 11; + +ASSERT NOT y AND (NOT z AND TRUE) => tmp3 = 0; +ASSERT y AND (NOT z AND TRUE) => tmp3 = 5; +ASSERT NOT y AND ( z AND TRUE) => tmp3 = 16; +ASSERT y AND ( z AND TRUE) => tmp3 = 21; + +ASSERT NOT x AND (NOT y AND TRUE) => tmp4 = 0; +ASSERT x AND (NOT y AND TRUE) => tmp4 = 4; +ASSERT NOT x AND ( y AND TRUE) => tmp4 = 6; +ASSERT x AND ( y AND TRUE) => tmp4 = 10; + +CHECKSAT; diff --git a/test/regress/regress1/arith/mod.02.smt2 b/test/regress/regress1/arith/mod.02.smt2 new file mode 100644 index 000000000..ee4333ea5 --- /dev/null +++ b/test/regress/regress1/arith/mod.02.smt2 @@ -0,0 +1,10 @@ +; EXPECT: unsat +(set-logic QF_NIA) +(set-info :smt-lib-version 2.0) +(set-info :status unsat) +(declare-fun n () Int) + +(assert (distinct n 0)) +(assert (> (mod n n) 0)) + +(check-sat) diff --git a/test/regress/regress1/arith/mod.03.smt2 b/test/regress/regress1/arith/mod.03.smt2 new file mode 100644 index 000000000..8a6ac51d7 --- /dev/null +++ b/test/regress/regress1/arith/mod.03.smt2 @@ -0,0 +1,11 @@ +; EXPECT: sat +(set-logic QF_NIA) +(set-info :smt-lib-version 2.0) +(set-info :status sat) +(declare-fun n () Int) +(declare-fun x () Int) + +(assert (< (mod x n) 0)) +(assert (< (div x n) 0)) + +(check-sat) diff --git a/test/regress/regress1/arith/mult.02.smt2 b/test/regress/regress1/arith/mult.02.smt2 new file mode 100644 index 000000000..57167fc76 --- /dev/null +++ b/test/regress/regress1/arith/mult.02.smt2 @@ -0,0 +1,13 @@ +; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic. +; EXPECT: The fact in question: (>= (* (- 1.0) (* n n)) (- 1.0)) +; EXPECT: ") +; EXIT: 1 +(set-logic QF_LRA) +(set-info :status unknown) +(declare-fun n () Real) + +; This example is test that LRA rejects multiplication terms + +(assert (= (* n n) 1)) + +(check-sat) diff --git a/test/regress/regress1/arith/problem__003.smt2 b/test/regress/regress1/arith/problem__003.smt2 new file mode 100644 index 000000000..7af727e2a --- /dev/null +++ b/test/regress/regress1/arith/problem__003.smt2 @@ -0,0 +1,21 @@ +(set-logic QF_LIA) +(set-info :source | +Alberto Griggio + +|) +(set-info :smt-lib-version 2.0) +(set-info :category "random") +(set-info :status sat) +(declare-fun x0 () Int) +(declare-fun x1 () Int) +(declare-fun x2 () Int) +(declare-fun x3 () Int) +(declare-fun x4 () Int) +(declare-fun x5 () Int) +(declare-fun x6 () Int) +(declare-fun x7 () Int) +(declare-fun x8 () Int) +(declare-fun x9 () Int) +(assert (let ((?v_3 (* 36 x4)) (?v_0 (* 37 x7)) (?v_21 (* 3 x1)) (?v_7 (* 1 x1)) (?v_2 (* 23 x0)) (?v_4 (* 37 x1)) (?v_23 (* 15 x8)) (?v_11 (* 24 x1)) (?v_14 (* 30 x5)) (?v_17 (* 31 x6)) (?v_19 (* 28 x5)) (?v_5 (* 26 x5)) (?v_12 (* 13 x5)) (?v_20 (* 5 x6)) (?v_1 (* (- 38) x0)) (?v_18 (* (- 33) x4)) (?v_22 (* (- 38) x1)) (?v_16 (* (- 24) x6)) (?v_6 (* (- 13) x1)) (?v_9 (* (- 8) x4)) (?v_13 (* (- 11) x9)) (?v_10 (* (- 6) x0)) (?v_15 (* (- 37) x7)) (?v_8 (* (- 3) x4))) (and (<= (+ (* 25 x2) (* 12 x8) (* 12 x7) ?v_3 (* (- 5) x6) (* (- 25) x7) (* 22 x5) (* 7 x6) (* (- 19) x5) (* 22 x8)) (- 4)) (<= (+ (* 16 x1) (* 27 x2) (* 36 x6) (* 0 x8) (* 18 x4) (* (- 6) x1) (* 3 x9) (* (- 31) x9) (* 8 x0) ?v_0) (- 39)) (<= (+ (* 22 x1) (* 14 x3) (* (- 1) x2) (* (- 29) x9) (* 25 x8) (* 27 x4) (* (- 8) x3) (* (- 17) x4) ?v_1 (* 7 x7)) (- 25)) (<= (+ (* 16 x2) (* 2 x5) (* (- 34) x8) (* 3 x7) ?v_21 (* (- 17) x9) (* (- 32) x4) (* (- 7) x9) (* (- 9) x2) (* 16 x8)) (- 39)) (<= (+ ?v_7 (* (- 8) x5) (* 6 x4) ?v_18 (* (- 37) x0) (* 16 x6) (* (- 12) x0) (* 22 x3) (* (- 36) x3) (* 36 x0)) 6) (<= (+ (* 9 x3) (* (- 36) x4) (* (- 32) x8) (* (- 16) x1) ?v_0 ?v_2 (* (- 6) x5) (* (- 31) x6) (* (- 5) x8) (* (- 15) x3)) (- 15)) (<= (+ (* 1 x8) (* (- 7) x6) ?v_4 (* 20 x2) ?v_1 (* 0 x0) (* (- 37) x8) (* 13 x3) (* (- 23) x7) (* 37 x9)) (- 14)) (<= (+ (* 34 x5) (* 10 x6) (* (- 3) x5) (* (- 38) x9) ?v_22 (* 19 x6) (* (- 39) x7) ?v_16 (* 12 x1) (* (- 3) x7)) 35) (<= (+ (* 20 x4) (* (- 39) x9) (* 24 x3) ?v_23 (* (- 18) x3) ?v_11 (* (- 23) x4) ?v_14 (* 11 x2) (* (- 1) x5)) (- 13)) (<= (+ (* 30 x9) ?v_17 (* 14 x2) ?v_6 (* (- 16) x8) (* 29 x1) (* (- 3) x6) ?v_9 (* (- 10) x8) ?v_19) (- 39)) (<= (+ (* 8 x4) (* 37 x2) ?v_13 (* 23 x2) ?v_2 (* (- 4) x1) (* 10 x5) (* (- 36) x0) (* (- 15) x0) (* (- 22) x3)) (- 24)) (<= (+ (* 38 x2) (* 23 x3) (* 12 x2) ?v_10 ?v_3 (* 29 x6) (* 4 x0) ?v_5 ?v_15 (* (- 10) x9)) 16) (<= (+ (* 31 x4) (* (- 26) x0) (* (- 19) x9) (* (- 21) x4) ?v_4 ?v_8 ?v_5 ?v_12 (* (- 20) x4) (* (- 31) x2)) (- 12)) (<= (+ (* 38 x9) (* (- 28) x1) (* 29 x0) (* 5 x1) (* (- 38) x8) ?v_6 (* (- 8) x2) ?v_20 (* 22 x7) (* (- 24) x9)) 10) (<= (+ ?v_7 ?v_8 (* 35 x5) (* 16 x3) (* 6 x7) ?v_9 (* (- 2) x3) (* (- 38) x5) ?v_10 (* (- 7) x4)) (- 29)) (<= (+ (* 11 x3) (* 5 x4) (* (- 2) x4) (* 37 x6) ?v_11 (* 0 x9) (* 25 x1) (* (- 3) x9) (* (- 33) x9) (* 19 x9)) (- 37)) (<= (+ ?v_12 (* 7 x4) ?v_13 ?v_14 (* (- 31) x0) (* (- 12) x6) (* (- 35) x0) (* 36 x2) (* (- 25) x3) ?v_15) (- 33)) (<= (+ (* 10 x4) ?v_16 (* 26 x6) ?v_17 ?v_18 (* (- 32) x5) (* 32 x2) (* 34 x8) (* 19 x1) ?v_1) (- 9)) (<= (+ ?v_12 (* (- 9) x3) (* (- 37) x3) (* 34 x4) (* 0 x1) ?v_19 (* 30 x6) (* (- 18) x4) (* 21 x5) (* (- 21) x9)) (- 9)) (<= (+ ?v_20 (* (- 30) x6) ?v_21 (* 9 x8) ?v_13 (* (- 28) x5) (* (- 14) x3) ?v_22 (* 5 x8) ?v_23) 35)))) +(check-sat) +(exit) |