Open
Description
[659] % z3release model_validate=true small.smt2
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
sat
(error "line 27 column 10: an invalid model was generated")
(
(define-fun a () Int
1)
(define-fun b () Bool
true)
(define-fun s () String
"220044AB")
)
[660] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Bool)
(declare-fun s () String)
(push)
(check-sat)
(assert (> (- (str.len s) 2 2 (+ 1 1 1)) 0))
(check-sat)
(assert (= "0" (str.at (str.substr s 2 2) 0)))
(check-sat)
(assert (not (= 1 (str.len (str.substr s 2 2)))))
(check-sat)
(assert (< (ite (str.prefixof "-" (str.substr s 0 (- 1 0))) (str.to_int (str.substr s 0 (+ 1 1))) 0) 255))
(check-sat)
(check-sat)
(check-sat)
(check-sat)
(check-sat)
(push)
(assert (> (str.len s) 0))
(check-sat)
(push)
(assert b)
(assert (> a 0))
(check-sat)
(assert (not (<= (ite (str.prefixof "-" (str.substr s 2 (- (+ 1 1 1 (- 1 1)) 1))) (- (str.to_int (str.substr (str.substr s 3 (- 3 1)) 1 (- (str.len (str.substr s 3 (+ 1 1 1 1 1))) 1)))) (str.to_int (str.substr s 3 (- (+ 1 1 1 1 1 1) 3)))) 255)))
(check-sat)
(check-sat)
(get-model)