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

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 53e050191a8b76672866c3a5543307034e574759..ac837b957bc1e21297ba70d2e9e6e01159730ddb 100644 (file)
--- 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 (file)
index 0000000..740a0dc
--- /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)