diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-11-30 15:14:36 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-11-30 15:14:36 +0000 |
commit | 03b766ec1f86976d602988581e5e47dbed31952c (patch) | |
tree | cd348a48b5c80bd7cf104c1b96a5c754f29e9717 /test | |
parent | ba522e64d0e9975cee8e3d33328e32c3b27ecd71 (diff) |
fix rewrite-rules syntax in regression
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress0/push-pop/bug326.smt2 | 6 |
1 files 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) |