diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-09 10:34:20 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-09-09 10:34:20 +0200 |
commit | 68d3518e446b1e0f1ac16c2146c162580fa377f9 (patch) | |
tree | 77822589380920f408557712c3be4411768bac0e /test/regress/regress0/strings/unsound-0908.smt2 | |
parent | d78d47eafdad2d76f681463787647cdf5892a2fd (diff) |
Fix bug in strings rewriter regarding lengths of substr terms.
Diffstat (limited to 'test/regress/regress0/strings/unsound-0908.smt2')
-rwxr-xr-x | test/regress/regress0/strings/unsound-0908.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2 new file mode 100755 index 000000000..cbaf5f5e4 --- /dev/null +++ b/test/regress/regress0/strings/unsound-0908.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_S)
+(set-info :status sat)
+(declare-const x String)
+(assert (= (str.len x) 1))
+;(assert (= x "X"))
+(assert
+ (or
+ (not (> (str.len x) 1))
+ (= (str.at x 1) "Z")
+ )
+)
+(check-sat)
|