Fix higher-order term indexing. (#1754)

2 files changed, 84 insertions, 0 deletions

diff --git a/test/regress/regress1/ho/fta0210.smt2 b/test/regress/regress1/ho/fta0210.smt2
new file mode 100644
index 000000000..9f0a39f25
--- /dev/null
+++ b/test/regress/regress1/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)
diff --git a/test/regress/regress1/ho/match-middle.smt2 b/test/regress/regress1/ho/match-middle.smt2
new file mode 100644
index 000000000..0485f9a6f
--- /dev/null
+++ b/test/regress/regress1/ho/match-middle.smt2
@@ -0,0 +1,20 @@
+; COMMAND-LINE: --uf-ho
+; EXPECT: unsat
+(set-logic UFLIA)
+(set-info :status unsat)
+(declare-fun f (Int Int Int) Int)
+(declare-fun h (Int Int Int) Int)
+(declare-fun g (Int Int) Int)
+(declare-fun a () Int)
+(declare-fun b () Int)
+(declare-fun c () Int)
+(declare-fun d () Int)
+
+(assert (or (= (f a) g) (= (h a) g)))
+
+(assert (= (f a b d) c))
+(assert (= (h a b d) c))
+
+(assert (forall ((x Int) (y Int)) (not (= (g x y) c))))
+
+(check-sat)