From 03b766ec1f86976d602988581e5e47dbed31952c Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 30 Nov 2012 15:14:36 +0000 Subject: [PATCH] fix rewrite-rules syntax in regression --- test/regress/regress0/push-pop/bug326.smt2 | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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) -- 2.30.2