diff options
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) |