diff options
Diffstat (limited to 'test/regress/regress0/ho/fta0210.smt2')
-rw-r--r-- | test/regress/regress0/ho/fta0210.smt2 | 64 |
1 files changed, 64 insertions, 0 deletions
diff --git a/test/regress/regress0/ho/fta0210.smt2 b/test/regress/regress0/ho/fta0210.smt2 new file mode 100644 index 000000000..9f0a39f25 --- /dev/null +++ b/test/regress/regress0/ho/fta0210.smt2 @@ -0,0 +1,64 @@ +; COMMAND-LINE: --uf-ho +; EXPECT: unsat +(set-logic ALL) +(declare-sort A$ 0) +(declare-sort Nat$ 0) +(declare-sort A_poly$ 0) +(declare-sort Nat_poly$ 0) +(declare-sort A_poly_poly$ 0) +(declare-fun p$ () A_poly$) +(declare-fun uu$ (A_poly$ (-> A_poly$ A_poly$) A_poly$) A_poly$) +(declare-fun one$ () Nat$) +(declare-fun suc$ (Nat$) Nat$) +(declare-fun uua$ (A_poly$) A_poly$) +(declare-fun uub$ (A$ (-> A$ A$) A$) A$) +(declare-fun uuc$ (A$) A$) +(declare-fun uud$ (Nat$ (-> Nat$ Nat$) Nat$) Nat$) +(declare-fun uue$ (Nat$) Nat$) +(declare-fun one$a () Nat_poly$) +(declare-fun one$b () A$) +(declare-fun one$c () A_poly$) +(declare-fun plus$ (A_poly$ A_poly$) A_poly$) +(declare-fun poly$ (A_poly$ A$) A$) +(declare-fun zero$ () A_poly$) +(declare-fun pCons$ (A$ A_poly$) A_poly$) +(declare-fun plus$a (Nat$ Nat$) Nat$) +(declare-fun plus$b (A$ A$) A$) +(declare-fun plus$c (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun poly$a (Nat_poly$ Nat$) Nat$) +(declare-fun poly$b (A_poly_poly$ A_poly$) A_poly$) +(declare-fun power$ (A$ Nat$) A$) +(declare-fun psize$ (A_poly$) Nat$) +(declare-fun times$ (A_poly$ A_poly$) A_poly$) +(declare-fun zero$a () Nat$) +(declare-fun zero$b () A$) +(declare-fun zero$c () Nat_poly$) +(declare-fun zero$d () A_poly_poly$) +(declare-fun pCons$a (Nat$ Nat_poly$) Nat_poly$) +(declare-fun pCons$b (A_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun power$a (A_poly$ Nat$) A_poly$) +(declare-fun power$b (Nat_poly$ Nat$) Nat_poly$) +(declare-fun power$c (Nat$ Nat$) Nat$) +(declare-fun psize$a (A_poly_poly$) Nat$) +(declare-fun times$a (Nat$ Nat$) Nat$) +(declare-fun times$b (A$ A$) A$) +(declare-fun times$c (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun times$d (A_poly_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun uminus$ (A_poly$) A_poly$) +(declare-fun uminus$a (A$) A$) +(declare-fun constant$ ((-> A$ A$)) Bool) +(declare-fun pcompose$ (A_poly$ A_poly$) A_poly$) +(declare-fun pcompose$a (Nat_poly$ Nat_poly$) Nat_poly$) +(declare-fun pcompose$b (A_poly_poly$ A_poly_poly$) A_poly_poly$) +(declare-fun poly_shift$ (Nat$ A_poly$) A_poly$) +(declare-fun fold_coeffs$ ((-> A_poly$ (-> (-> A_poly$ A_poly$) (-> A_poly$ A_poly$))) A_poly_poly$ (-> A_poly$ A_poly$)) (-> A_poly$ A_poly$)) +(declare-fun poly_cutoff$ (Nat$ A_poly$) A_poly$) +(declare-fun fold_coeffs$a ((-> A$ (-> (-> A$ A$) (-> A$ A$))) A_poly$ (-> A$ A$)) (-> A$ A$)) +(declare-fun fold_coeffs$b ((-> Nat$ (-> (-> Nat$ Nat$) (-> Nat$ Nat$))) Nat_poly$ (-> Nat$ Nat$)) (-> Nat$ Nat$)) + +(assert (! (forall ((?v0 A$)) (= (poly$ zero$ ?v0) zero$b)) :named a14)) +(assert (! (forall ((?v0 (-> A$ A$))) (= (constant$ ?v0) (forall ((?v1 A$) (?v2 A$)) (= (?v0 ?v1) (?v0 ?v2))))) :named a69)) +(assert (! (not (constant$ (poly$ zero$))) :named a206)) + +(check-sat) +;(get-proof) |