From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Wed, 7 Jul 2010 16:02:10 +0000 (+0000)
Subject: Fixing test plus-mult.cvc by making it linear (Fixes: #184)
X-Git-Tag: cvc5-1.0.0~8921
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=26c1b20086b26da79d938057b7761de95fabf731;p=cvc5.git

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 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