1 files changed, 35 insertions, 0 deletions
diff --git a/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2 b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
new file mode 100644
index 000000000..9dd95aeae
--- /dev/null
+++ b/test/regress/regress1/ho/bug_freevar_PHI004^4-delta.smt2
@@ -0,0 +1,35 @@
+; COMMAND-LINE: --uf-ho --finite-model-find --no-check-models
+; EXPECT: sat
+
+(set-logic ALL)
+(declare-sort $$unsorted 0)
+(declare-sort qML_mu 0)
+(declare-sort qML_i 0)
+(declare-fun scott_G (qML_mu qML_i) Bool)
+(declare-fun scott_P ((-> qML_mu qML_i Bool) qML_i) Bool)
+
+(assert
+  (=
+    scott_G
+    (lambda ((X qML_mu) (__flatten_var_0 qML_i))
+      (forall ((BOUND_VARIABLE_292 (-> qML_mu qML_i Bool)))
+        (or
+          (not (scott_P BOUND_VARIABLE_292 __flatten_var_0))
+          (BOUND_VARIABLE_292 X __flatten_var_0)
+          ) ))))
+
+(assert
+  (forall ((X_1 qML_i))
+    (scott_P
+      (lambda ((X qML_mu) (__flatten_var_0 qML_i))
+        (forall ((BOUND_VARIABLE_292 (-> qML_mu qML_i Bool)))
+          (or
+            (not (scott_P BOUND_VARIABLE_292 __flatten_var_0))
+            (BOUND_VARIABLE_292 X __flatten_var_0)) ))
+      X_1
+      )
+    ))
+
+
+
+(check-sat)
+\ No newline at end of file