7 files changed, 67 insertions, 3 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d9076c81b..4937c8481 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -660,11 +660,14 @@ set(regress_0_tests
   regress0/ho/issue6536.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
+  regress0/ho/lazy-lambda-model.smt2
   regress0/ho/match-middle.smt2
   regress0/ho/modulo-func-equality.smt2
   regress0/ho/qgu-fuzz-ho-1-dd.smt2
   regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
   regress0/ho/shadowing-defs.smt2
+  regress0/ho/simple-conf-lazy-lambda-lift.smt2
+  regress0/ho/simple-conf-lazy-lambda-lift-app.smt2
   regress0/ho/simple-matching-partial.smt2
   regress0/ho/simple-matching.smt2
   regress0/ho/trans.smt2
@@ -1604,6 +1607,7 @@ set(regress_1_tests
   regress1/bags/intersection_min1.smt2
   regress1/bags/intersection_min2.smt2
   regress1/bags/issue5759.smt2
+  regress1/bags/map-lazy-lam.smt2
   regress1/bags/map1.smt2
   regress1/bags/map2.smt2
   regress1/bags/map3.smt2
@@ -1728,8 +1732,10 @@ set(regress_1_tests
   regress1/fmf/with-ind-104-core.smt2
   regress1/gensys_brn001.smt2
   regress1/ho/bug_freeVar_BDD_General_data_270.p
+  regress1/ho/bug_freevar_PHI004^4-delta.smt2
   regress1/ho/bound_var_bug.p
   regress1/ho/fta0328.lfho.p
+  regress1/ho/ho-fun-sharing-dd.smt2
   regress1/ho/issue3136-fconst-bool-bool.smt2
   regress1/ho/issue4065-no-rep.smt2
   regress1/ho/issue4092-sinf.smt2
@@ -2805,8 +2811,6 @@ set(regression_disabled_tests
   ###
   regress1/bug472.smt2
   regress1/datatypes/non-simple-rec-set.smt2
-  # disabled temporarily until lazy lambda handling is merged
-  regress1/ho/bug_freevar_PHI004^4-delta.smt2
   # results in an assertion failure (see issue #1650).
   regress1/ho/hoa0102.smt2
   # after disallowing solving for terms with quantifiers
diff --git a/test/regress/regress0/ho/lazy-lambda-model.smt2 b/test/regress/regress0/ho/lazy-lambda-model.smt2
new file mode 100644
index 000000000..71df017e9
--- /dev/null
+++ b/test/regress/regress0/ho/lazy-lambda-model.smt2
@@ -0,0 +1,16 @@
+; COMMAND-LINE: --uf-lazy-ll
+; EXPECT: sat
+(set-logic HO_ALL)
+(declare-fun g (Int) Int)
+(declare-fun h (Int) Int)
+(define-fun f ((x Int)) Int (ite (> x 0) (* 2 x) x))
+
+(declare-fun a () Int)
+(declare-fun b () Int)
+
+
+(assert (or (= f g) (= f h)))
+
+(assert (and (= (h a) 26) (= (g b) 26)))
+
+(check-sat)
diff --git a/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2 b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2
new file mode 100644
index 000000000..ab949c40c
--- /dev/null
+++ b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift-app.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --uf-lazy-ll
+; EXPECT: unsat
+(set-logic HO_ALL)
+(set-info :status unsat)
+(define-fun f ((x Int)) Int (+ x 1))
+(declare-fun g (Int) Int)
+(declare-fun h (Int) Int)
+
+(assert (or (= f g) (= f h)))
+
+(assert (= (g 4) 0))
+(assert (= (h 4) 8))
+
+(check-sat)
diff --git a/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2 b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2
new file mode 100644
index 000000000..d11a4418b
--- /dev/null
+++ b/test/regress/regress0/ho/simple-conf-lazy-lambda-lift.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --uf-lazy-ll
+; EXPECT: unsat
+(set-logic HO_ALL)
+(set-info :status unsat)
+(define-fun f ((x Int)) Int (+ x 1))
+(define-fun g ((x Int)) Int (+ x 2))
+(define-fun h ((x Int)) Int 6)
+
+(assert (or (= f g) (= f h)))
+
+(check-sat)
diff --git a/test/regress/regress1/bags/map-lazy-lam.smt2 b/test/regress/regress1/bags/map-lazy-lam.smt2
new file mode 100644
index 000000000..c99bab7c9
--- /dev/null
+++ b/test/regress/regress1/bags/map-lazy-lam.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --fmf-bound --uf-lazy-ll
+; EXPECT: sat
+(set-logic HO_ALL)
+(define-fun f ((x String)) Int 1)
+(define-fun cardinality ((A (Bag String))) Int
+  (bag.count 1 (bag.map f A)))
+(declare-fun A () (Bag String))
+(assert (= (cardinality A) 20))
+(check-sat)
diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
index 7c9de4c49..0155eecb2 100644
--- a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
+++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find -q --decision=justification-old
+; COMMAND-LINE: --finite-model-find --decision=justification-old --uf-lazy-ll -q
 ; EXPECT: sat
 
 (set-logic HO_ALL)
diff --git a/test/regress/regress1/ho/ho-fun-sharing-dd.smt2 b/test/regress/regress1/ho/ho-fun-sharing-dd.smt2
new file mode 100644
index 000000000..300dc26de
--- /dev/null
+++ b/test/regress/regress1/ho/ho-fun-sharing-dd.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: unsat
+(set-logic HO_ALL)
+(declare-sort n 0)
+(declare-fun x () n)
+(declare-fun s (n) n)
+(declare-fun t ((-> n Bool)) Bool)
+(assert (forall ((X n)) (t (lambda ((Xu n)) (= X (s Xu))))))
+(assert (not (t (lambda ((Xu n)) (= x (s Xu))))))
+(check-sat)