diff options
Diffstat (limited to 'test/regress/regress0/ho/hoa0008.smt2')
-rw-r--r-- | test/regress/regress0/ho/hoa0008.smt2 | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/test/regress/regress0/ho/hoa0008.smt2 b/test/regress/regress0/ho/hoa0008.smt2 new file mode 100644 index 000000000..f4833aadf --- /dev/null +++ b/test/regress/regress0/ho/hoa0008.smt2 @@ -0,0 +1,68 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) +(declare-sort A$ 0) +(declare-sort Com$ 0) +(declare-sort Loc$ 0) +(declare-sort Nat$ 0) +(declare-sort Pname$ 0) +(declare-sort State$ 0) +(declare-sort Vname$ 0) +(declare-sort Literal$ 0) +(declare-sort Natural$ 0) +(declare-sort Typerep$ 0) +(declare-sort A_triple$ 0) +(declare-sort Com_option$ 0) +(declare-fun p$ () (-> A$ (-> State$ Bool))) +(declare-fun q$ () (-> A$ (-> State$ Bool))) +(declare-fun pn$ () Pname$) +(declare-fun wt$ (Com$) Bool) +(declare-fun ass$ (Vname$ (-> State$ Nat$)) Com$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun the$ (Com_option$) Com$) +(declare-fun body$ (Pname$) Com$) +(declare-fun call$ (Vname$ Pname$ (-> State$ Nat$)) Com$) +(declare-fun cond$ ((-> State$ Bool) Com$ Com$) Com$) +(declare-fun none$ () Com_option$) +(declare-fun plus$ (Nat$ Nat$) Nat$) +(declare-fun semi$ (Com$ Com$) Com$) +(declare-fun size$ (A_triple$) Nat$) +(declare-fun skip$ () Com$) +(declare-fun some$ (Com$) Com_option$) +(declare-fun suc$a (Natural$) Natural$) +(declare-fun zero$ () Nat$) +(declare-fun body$a (Pname$) Com_option$) +(declare-fun evalc$ (Com$ State$ State$) Bool) +(declare-fun evaln$ (Com$ State$ Nat$ State$) Bool) +(declare-fun local$ (Loc$ (-> State$ Nat$) Com$) Com$) +(declare-fun plus$a (Natural$ Natural$) Natural$) +(declare-fun size$a (Com$) Nat$) +(declare-fun size$b (Natural$) Nat$) +(declare-fun size$c (Bool) Nat$) +(declare-fun size$d (Com_option$) Nat$) +(declare-fun size$e (Typerep$) Nat$) +(declare-fun size$f (Literal$) Nat$) +(declare-fun while$ ((-> State$ Bool) Com$) Com$) +(declare-fun zero$a () Natural$) +(declare-fun triple$ ((-> A$ (-> State$ Bool)) Com$ (-> A$ (-> State$ Bool))) A_triple$) +(declare-fun rec_bool$ (Nat$ Nat$) (-> Bool Nat$)) +(declare-fun size_com$ (Com$) Nat$) +(declare-fun size_bool$ (Bool) Nat$) +(declare-fun wT_bodies$ () Bool) +(declare-fun size_option$ ((-> Com$ Nat$)) (-> Com_option$ Nat$)) +(declare-fun size_triple$ ((-> A$ Nat$) A_triple$) Nat$) +(declare-fun size_natural$ (Natural$) Nat$) +(declare-fun triple_valid$ (Nat$ A_triple$) Bool) +(assert (! (not (triple_valid$ zero$ (triple$ p$ (body$ pn$) q$))) :named a0)) + +(assert (! (forall ((?v0 Nat$) (?v1 (-> A$ (-> State$ Bool))) (?v2 Com$) (?v3 (-> A$ (-> State$ Bool)))) (= (triple_valid$ ?v0 (triple$ ?v1 ?v2 ?v3)) (forall ((?v4 A$) (?v5 State$)) (=> (?v1 ?v4 ?v5) (forall ((?v6 State$)) (=> (evaln$ ?v2 ?v5 ?v0 ?v6) (?v3 ?v4 ?v6))))))) :named a6)) + +(assert (! (= (size_bool$ true) zero$) :named a13)) +(assert (! (= size_bool$ (rec_bool$ zero$ zero$)) :named a14)) + +(assert (! (forall ((?v0 Nat$)) (not (= zero$ (suc$ ?v0)))) :named a37)) + +(assert (! (forall ((?v0 Pname$) (?v1 State$) (?v2 Nat$) (?v3 State$)) (=> (and (evaln$ (body$ ?v0) ?v1 ?v2 ?v3) (forall ((?v4 Nat$)) (=> (and (= ?v2 (suc$ ?v4)) (evaln$ (the$ (body$a ?v0)) ?v1 ?v4 ?v3)) false))) false)) :named a204)) + +(check-sat) +;(get-proof) |