Merge branch 'master' of https://github.com/z3prover/z3test

Z3Prover · Dec 19, 2021 · ad9236f · ad9236f
2 parents d65a671 + 9b0c1d4
commit ad9236f
Show file tree

Hide file tree

Showing 3 changed files with 15 additions and 6 deletions.
diff --git a/regressions/issues/5693.smt2 b/regressions/issues/5693.smt2
diff --git a/regressions/issues/5693.expected.out → regressions/smt2/5693.expected.out b/regressions/issues/5693.expected.out → regressions/smt2/5693.expected.out
@@ -1 +1,2 @@
 unsat
+unsat
diff --git a/regressions/smt2/5693.smt2 b/regressions/smt2/5693.smt2
@@ -0,0 +1,14 @@
+(assert (let ((a!1 (re.++ (str.to_re "a")
+                  (re.* (re.++ (str.to_re "b") (str.to_re "a")))))
+      (a!2 (re.++ (re.* (re.++ (str.to_re "a") (str.to_re "b")))
+                  (str.to_re "a"))))
+  (distinct (re.++ a!1 a!1) (re.++ a!2 a!2))))
+(check-sat)
+(reset)
+(declare-const s String)
+(assert (let ((a!1 (re.++ (str.to_re "a")
+(re.* (re.++ (str.to_re "b") (str.to_re "a")))))
+(a!2 (re.++ (re.* (re.++ (str.to_re "a") (str.to_re "b")))
+(str.to_re "a"))))
+(str.in.re s (re.diff (re.++ a!1 a!1) (re.++ a!2 a!2)))))
+(check-sat)