From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 23 Jun 2021 22:07:56 +0000 (-0300)
Subject: [regressions] Adding regression from #5371 (#6791)
X-Git-Tag: cvc5-1.0.0~1562
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c4dca0e5430e92c6a412b9fff343ff81182a0c2b;p=cvc5.git

[regressions] Adding regression from #5371 (#6791)
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 53e050191..ac837b957 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -632,6 +632,7 @@ set(regress_0_tests
   regress0/ho/issue4477.smt2
   regress0/ho/issue4990-care-graph.smt2
   regress0/ho/issue5233-part1-usort-owner.smt2
+  regress0/ho/issue5371.smt2
   regress0/ho/issue6526.smt2
   regress0/ho/ite-apply-eq.smt2
   regress0/ho/lambda-equality-non-canon.smt2
diff --git a/test/regress/regress0/ho/issue5371.smt2 b/test/regress/regress0/ho/issue5371.smt2
new file mode 100644
index 000000000..740a0dc23
--- /dev/null
+++ b/test/regress/regress0/ho/issue5371.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --strings-exp
+; EXPECT: sat
+(set-logic HO_ALL)
+(declare-fun a (Bool) Bool)
+(assert (a false))
+(assert (a true))
+(check-sat)