Add regression for fixed issue (#8213)

Fixes #5815.

This adds the regression, in theory I still think it is possible for the assertion to fail, but I don't think it is worth pursuing right now.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 807abb4c2507ccf7dee0693e888108cb13835931..55d81d96434e37f81d0be51622c005ad43d5d702 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1330,6 +1330,7 @@ set(regress_0_tests
   regress0/strings/issue5745-eager-pp.smt2
   regress0/strings/issue5767-eager-pp.smt2
   regress0/strings/issue5771-eager-pp.smt2
+  regress0/strings/issue5815-ndet-string-ent.smt2
   regress0/strings/issue5816-re-kind.smt2
   regress0/strings/issue5915-repl-ctn-rewrite.smt2
   regress0/strings/issue6203-3-unfold-trivial-true.smt2

diff --git a/test/regress/regress0/strings/issue5815-ndet-string-ent.smt2 b/test/regress/regress0/strings/issue5815-ndet-string-ent.smt2
new file mode 100644 (file)
index 0000000..abf5c2b
--- /dev/null
+++ b/test/regress/regress0/strings/issue5815-ndet-string-ent.smt2
@@ -0,0 +1,7 @@
+(set-logic ALL)
+(set-info :status sat)
+(declare-fun a () String)
+(assert (= (str.substr (str.substr a (+ (+ 1 0) 1)
+    (- (str.len (str.substr (str.substr (str.substr a 1 (- (+ (str.len a) 1) 1)) 1 (- (+ 1 (+ 1 1)) 1)) 
+    1 (- (str.len a) 1))) 1)) 0 0) a))
+(check-sat)