From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Wed, 7 Jul 2010 16:25:36 +0000 (+0000)
Subject: Making plus-mult.cvc test a bit more torturous (as enabled by r744)
X-Git-Tag: cvc5-1.0.0~8919
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=97eb2d77fddb9c690cc2ebc2caff98d62467b671;p=cvc5.git

Making plus-mult.cvc test a bit more torturous (as enabled by r744)
---

diff --git a/test/regress/regress0/precedence/plus-mult.cvc b/test/regress/regress0/precedence/plus-mult.cvc
index 2d87cc44a..ecd34f583 100644
--- a/test/regress/regress0/precedence/plus-mult.cvc
+++ b/test/regress/regress0/precedence/plus-mult.cvc
@@ -1,8 +1,8 @@
 % EXPECT: VALID
 % Simple test for right precedence of plus/minus and mult/divide
 
-a, b, c, d: INT;
+a, b, c, d, e: INT;
 
-QUERY (a + 2 * b - c = 3 * a + 4 * b) <=> 
-  (((a + (2 * b)) - c) = ((3 * a) + (4 * b)));
+QUERY (a + 2 * b / 3 - c / 4 * 5 + d / 6 - e ) =
+  ((((a + ((2 * b) / 3)) - ((c / 4) * 5)) + (d / 6)) - e);
 % EXIT: 20