diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-09 11:58:08 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-09 11:58:08 +0000 |
commit | bdaa3049467fd17d3fb95701f7946a4bf0f5206a (patch) | |
tree | 7b770e107d3a625f266381141d3489cc23fecafe /test/regress/regress0/rewriterules/simulate_rewriting.smt2 | |
parent | 914dc99c1b89cf7203dc20296e8279786af202f9 (diff) |
fix beta reduction in both preRewrite() *and* postRewrite(), related to bug 417. oops. also fix spelling on "rewritting" test
Diffstat (limited to 'test/regress/regress0/rewriterules/simulate_rewriting.smt2')
-rw-r--r-- | test/regress/regress0/rewriterules/simulate_rewriting.smt2 | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/regress/regress0/rewriterules/simulate_rewriting.smt2 b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 new file mode 100644 index 000000000..d1d88a549 --- /dev/null +++ b/test/regress/regress0/rewriterules/simulate_rewriting.smt2 @@ -0,0 +1,24 @@ +;; A new fast tableau-base ... Domenico Cantone et Calogero G.Zarba +(set-logic AUFLIA) +(set-info :status sat) + +(declare-sort elt1 0) +(declare-sort elt2 0) + +(declare-fun g (elt2) Bool) + +(declare-fun p (elt1 elt1) Bool) +(declare-fun f (elt2) elt1) +(declare-fun c1 () elt1) +(declare-fun c2 () elt1) + +(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c2)) :rewrite-rule))) +(assert (forall ((?e elt2)) (! (=> (g ?e) (= (f ?e) c1)) :rewrite-rule))) + +(declare-fun e () elt2) + +(assert (not (=> (g e) (=> (p c1 c2) (p (f e) (f e)))) )) + +(check-sat) + +(exit) |