diff options
Diffstat (limited to 'test/regress/regress2/strings/proof-fail-083021-delta.smt2')
| -rw-r--r-- | test/regress/regress2/strings/proof-fail-083021-delta.smt2 | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/test/regress/regress2/strings/proof-fail-083021-delta.smt2 b/test/regress/regress2/strings/proof-fail-083021-delta.smt2 new file mode 100644 index 000000000..981102b7c --- /dev/null +++ b/test/regress/regress2/strings/proof-fail-083021-delta.smt2 @@ -0,0 +1,12 @@ +(set-logic QF_SLIA) +(set-info :status unsat) +(declare-const x Bool) +(declare-const x1 Int) +(declare-fun s () String) +(assert (ite (str.prefixof "-" (str.substr s 0 1)) (= 0 (str.to_int (str.substr (str.substr s 0 (+ 1 1)) 1 (- (str.len (str.substr s 0 (+ 1 1))) 1)))) true)) +(assert (not (<= (- (str.len s) 1 (+ 1 1) 1) 3))) +(assert (ite x true (> 1 (str.len (str.substr s (+ 1 1 1 1) (- (str.len s) (+ 1 1 1 1 1))))))) +(assert (ite (str.prefixof "-" (str.substr s (+ 1 1) 1)) (= 0 (str.to_int (str.substr (str.substr s (+ 1 1) (+ 1 1 1)) 1 (- (str.len (str.substr s 1 x1)) 1)))) true)) +(assert (str.in_re s (re.+ (re.range "0" "9")))) +(assert (not (<= (str.to_int (str.substr s 0 (+ 1 1))) 255))) +(check-sat) |