From 1261a85ddb6daa08561744514ea89bbe1657f366 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 2 Mar 2022 22:26:54 -0600 Subject: [PATCH] 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. --- test/regress/CMakeLists.txt | 1 + .../regress0/strings/issue5815-ndet-string-ent.smt2 | 7 +++++++ 2 files changed, 8 insertions(+) create mode 100644 test/regress/regress0/strings/issue5815-ndet-string-ent.smt2 diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 807abb4c2..55d81d964 100644 --- 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 index 000000000..abf5c2b55 --- /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) -- 2.30.2