1 files changed, 50 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2 b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
new file mode 100644
index 000000000..9211adfb5
--- /dev/null
+++ b/test/regress/regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
@@ -0,0 +1,50 @@
+; COMMAND-LINE:  --uf-ho --finite-model-find --no-check-models
+; EXPECT: sat
+
+
+(set-logic ALL)
+(declare-sort $$unsorted 0)
+
+(declare-fun mvalid ((-> $$unsorted Bool)) Bool)
+(assert (= mvalid (lambda ((Phi (-> $$unsorted Bool))) (forall ((W $$unsorted)) (Phi W) ))))
+
+(declare-fun mforall_prop ((-> (-> $$unsorted Bool) $$unsorted Bool) $$unsorted) Bool)
+(assert (= mforall_prop
+          (lambda ((Phi (-> (-> $$unsorted Bool) $$unsorted Bool)) (W $$unsorted))
+            (forall ((P (-> $$unsorted Bool))) (Phi P W) ))))
+
+(declare-fun mnot ((-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mnot (lambda ((Phi (-> $$unsorted Bool)) (W $$unsorted)) (not (Phi W)))))
+
+(declare-fun mor ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mor
+          (lambda ((Phi (-> $$unsorted Bool)) (Psi (-> $$unsorted Bool)) (W $$unsorted))
+            (or (Phi W) (Psi W)))))
+
+(declare-fun mimplies ((-> $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mimplies
+          (lambda (
+                    (Phi (-> $$unsorted Bool))
+                    (Psi (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted))
+            (mor (mnot Phi) Psi __flatten_var_0))))
+
+(declare-fun mbox ((-> $$unsorted $$unsorted Bool) (-> $$unsorted Bool) $$unsorted) Bool)
+(assert (= mbox
+          (lambda ((R (-> $$unsorted $$unsorted Bool)) (Phi (-> $$unsorted Bool)) (W $$unsorted))
+            (forall ((V $$unsorted)) (or (not (R W V)) (Phi V)) ))))
+
+(assert (not (forall ((R (-> $$unsorted $$unsorted Bool)))
+               (mvalid
+                 (mforall_prop
+                   (lambda ((A (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted))
+                     (mforall_prop
+                       (lambda ((B (-> $$unsorted Bool)) (__flatten_var_0 $$unsorted))
+                         (mimplies
+                           (mbox R (mor A B))
+                           (mor
+                             (mbox R A)
+                             (mbox R B))
+                           __flatten_var_0))
+                       __flatten_var_0)))) )))
+
+(check-sat)