From 26c1b20086b26da79d938057b7761de95fabf731 Mon Sep 17 00:00:00 2001 From: "Christopher L. Conway" Date: Wed, 7 Jul 2010 16:02:10 +0000 Subject: [PATCH] Fixing test plus-mult.cvc by making it linear (Fixes: #184) --- test/regress/regress0/precedence/Makefile.am | 4 +--- test/regress/regress0/precedence/plus-mult.cvc | 4 ++-- 2 files changed, 3 insertions(+), 5 deletions(-) diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 9b1f1c1e2..88defc40b 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -16,15 +16,13 @@ TESTS = \ implies-or.cvc \ not-and.cvc \ not-eq.cvc \ + plus-mult.cvc \ or-implies.cvc \ or-xor.cvc \ xor-or.cvc \ xor-and.cvc \ xor-assoc.cvc -# Causes failure in TheoryArith: -# plus-mult.cvc - EXTRA_DIST = $(TESTS) #if CVC4_BUILD_PROFILE_COMPETITION diff --git a/test/regress/regress0/precedence/plus-mult.cvc b/test/regress/regress0/precedence/plus-mult.cvc index c72b30d1c..2d87cc44a 100644 --- a/test/regress/regress0/precedence/plus-mult.cvc +++ b/test/regress/regress0/precedence/plus-mult.cvc @@ -3,6 +3,6 @@ a, b, c, d: INT; -QUERY (a + b * c - d = a * b + c * d) <=> - (((a + (b * c)) - d) = ((a * b) + (c * d))); +QUERY (a + 2 * b - c = 3 * a + 4 * b) <=> + (((a + (2 * b)) - c) = ((3 * a) + (4 * b))); % EXIT: 20 -- 2.30.2