1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/str-code-unsat-3.smt2 b/test/regress/regress1/strings/str-code-unsat-3.smt2
new file mode 100644
index 000000000..fa34785c2
--- /dev/null
+++ b/test/regress/regress1/strings/str-code-unsat-3.smt2
@@ -0,0 +1,21 @@
+(set-logic QF_SLIA)
+(set-info :status unsat)
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (>= (str.code x) 65))
+(assert (<= (str.code x) 75))
+
+(assert (>= (str.code y) 65))
+(assert (<= (str.code y) 75))
+
+(assert (>= (str.code z) 65))
+(assert (<= (str.code z) 75))
+
+(assert (= (+ (str.code x) (str.code y)) 140))
+(assert (= (+ (str.code x) (str.code z)) 141))
+
+(assert (distinct x y z "B" "C" "D" "E"))
+
+(check-sat)