From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 30 Nov 2012 15:14:36 +0000 (+0000)
Subject: fix rewrite-rules syntax in regression
X-Git-Tag: cvc5-1.0.0~7522
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03b766ec1f86976d602988581e5e47dbed31952c;p=cvc5.git

fix rewrite-rules syntax in regression
---

diff --git a/test/regress/regress0/push-pop/bug326.smt2 b/test/regress/regress0/push-pop/bug326.smt2
index 04b417e17..d32d6fddf 100644
--- a/test/regress/regress0/push-pop/bug326.smt2
+++ b/test/regress/regress0/push-pop/bug326.smt2
@@ -6,13 +6,13 @@
 (declare-fun R (Int Int) Bool)
 
 ;; reflexive
-(assert-rewrite ((x Int)) () (R x x) true ())
+(assert-rewrite ((x Int)) () () (R x x) true)
 
 ;; anti-symmetric
-(assert-reduction ((x Int) (y Int)) () ((R x y) (R y x)) (= x y) ())
+(assert-reduction ((x Int) (y Int)) () () ((R x y) (R y x)) (= x y))
 
 ;; transitive
-(assert-propagation ((x Int) (y Int) (z Int)) () ((R x y) (R y z)) (R x z) ())
+(assert-propagation ((x Int) (y Int) (z Int)) () () ((R x y) (R y z)) (R x z))
 
 
 (declare-fun e1 () Int)