Fixing test plus-mult.cvc by making it linear (Fixes: #184)

diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am
index 9b1f1c1e210a7cd1c7e59bcf95da00c0fce3f736..88defc40bad4aada85de93e62ff1db88af943325 100644 (file)
--- 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 c72b30d1c0ed32b30e9746c42fe71ebbe5557cba..2d87cc44a4ea335db9f108f5263eef7ea98ed33e 100644 (file)
--- 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