diff options
Diffstat (limited to 'test/regress/regress1/fmf/lst-no-self-rev-exp.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 | 21 |
1 files changed, 10 insertions, 11 deletions
diff --git a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 index d55e15925..b2c42d7c5 100644 --- a/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 +++ b/test/regress/regress1/fmf/lst-no-self-rev-exp.smt2 @@ -1,11 +1,11 @@ -; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel --lang=smt2.5 +; COMMAND-LINE: --finite-model-find --dt-rewrite-error-sel ; EXPECT: sat (set-logic ALL_SUPPORTED) -(declare-datatypes () ((Nat (succ (pred Nat)) (zero)) (Lst (cons (hd Nat) (tl Lst)) (nil)))) +(declare-datatypes ((Nat 0) (Lst 0)) (((succ (pred Nat)) (zero)) ((cons (hd Nat) (tl Lst)) (nil)))) (declare-fun app (Lst Lst) Lst) (declare-fun rev (Lst) Lst) - + (declare-sort I_app 0) (declare-sort I_rev 0) @@ -20,16 +20,15 @@ (declare-fun xs () Lst) (assert (and - -(forall ((?i I_app)) (= (app (app_0_3 ?i) (app_1_4 ?i)) (ite (is-cons (app_0_3 ?i)) (cons (hd (app_0_3 ?i)) (app (tl (app_0_3 ?i)) (app_1_4 ?i))) (app_1_4 ?i))) ) - -(forall ((?i I_rev)) (= (rev (rev_0_5 ?i)) (ite (is-cons (rev_0_5 ?i)) (app (rev (tl (rev_0_5 ?i))) (cons (hd (rev_0_5 ?i)) nil)) nil)) ) -(forall ((?i I_rev)) (or (not (is-cons (rev_0_5 ?i))) (and (not (forall ((?z I_app)) (not (and (= (app_0_3 ?z) (rev (tl (rev_0_5 ?i)))) (= (app_1_4 ?z) (cons (hd (rev_0_5 ?i)) nil)))) )) (not (forall ((?z I_rev)) (not (= (rev_0_5 ?z) (tl (rev_0_5 ?i)) )) )))) ) +(forall ((?i I_app)) (= (app (app_0_3 ?i) (app_1_4 ?i)) (ite ((_ is cons) (app_0_3 ?i)) (cons (hd (app_0_3 ?i)) (app (tl (app_0_3 ?i)) (app_1_4 ?i))) (app_1_4 ?i))) ) + +(forall ((?i I_rev)) (= (rev (rev_0_5 ?i)) (ite ((_ is cons) (rev_0_5 ?i)) (app (rev (tl (rev_0_5 ?i))) (cons (hd (rev_0_5 ?i)) nil)) nil)) ) + +(forall ((?i I_rev)) (or (not ((_ is cons) (rev_0_5 ?i))) (and (not (forall ((?z I_app)) (not (and (= (app_0_3 ?z) (rev (tl (rev_0_5 ?i)))) (= (app_1_4 ?z) (cons (hd (rev_0_5 ?i)) nil)))) )) (not (forall ((?z I_rev)) (not (= (rev_0_5 ?z) (tl (rev_0_5 ?i)) )) )))) ) (not (or (= xs (rev xs)) (forall ((?z I_rev)) (not (= (rev_0_5 ?z) xs)) ))) - + )) - -(check-sat) +(check-sat) |