1 files changed, 68 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/hoa0008.smt2 b/test/regress/regress1/ho/hoa0008.smt2
new file mode 100644
index 000000000..f4833aadf
--- /dev/null
+++ b/test/regress/regress1/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)