feat: add z3str3 soundness issue

nicdard · Jul 15, 2022 · 5bb348b · 5bb348b
1 parent 1c3c16e
commit 5bb348b
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 0 deletions.
diff --git a/bugs/README.md b/bugs/README.md
@@ -7,4 +7,5 @@
 | [QF_NRA 1](z3/qf_nra-1.smt2) | QF_NRA | Segfault            | [#6044](https://github.com/Z3Prover/z3/issues/6044)                         | 20/05/22 |
 | [QF_S 1](z3/qf_s-1.smt2)     | QF_S   | Memory Leak         | [#6076](https://github.com/Z3Prover/z3/issues/6076)                         | 04/06/22 |
 | [QF_BV 1](z3/qf_bv-1.smt2)   | QF_BV  | Assertion Violation | [#6143](https://github.com/Z3Prover/z3/issues/6143)                         | 07/07/22 |
+| [QF_S 2](z3/qf_s-2.smt2)     | QF_S   | Soundness           | [#6159](https://github.com/Z3Prover/z3/issues/6159)                         | 14/07/22 |
 
diff --git a/bugs/z3/qf_s-2.smt2 b/bugs/z3/qf_s-2.smt2
@@ -0,0 +1,19 @@
+(declare-fun s () String)
+(declare-fun r () String)
+(assert 
+  (and 
+    (= 
+      "\u{2f}" (str.substr s 0 (str.len "lo"))) 
+      (str.in_re r (re.++ (re.* re.allchar) (re.++ (str.to_re "\u{2f}\") (re.* re.allchar)))
+    ) 
+    (= 
+      (str.substr r 0 (str.len (str.++ r ""))) (str.++ (str.++ (str.substr s 0 (str.len "lo")) s) 
+      (str.substr s 0 1))
+    )
+  )
+)
+(check-sat)
+
+
+; $ z3
+; sat, expected unsat