You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
[537] % z3release model_validate=true small.smt2
sat
sat
(error "line 7 column 10: an invalid model was generated")
(
(define-fun b () Int
1)
(define-fun a ((x!0 Int)) Int
0)
)
[538] % cat small.smt2
(declare-fun a (Int) Int)
(declare-fun b () Int)
(push)
(assert (> b 0))
(check-sat)
(assert (< (a 1) (a b)))
(check-sat)
(get-model)
The text was updated successfully, but these errors were encountered:
[546] % z3release model_validate=true small.smt2
sat
sat
sat
(error "line 7 column 10: an invalid model was generated")
(
(define-fun a () Int
0)
(define-fun b ((x!0 Int)) Bool
true)
)
[547] % cat small.smt2
(declare-fun a () Int)
(check-sat)
(declare-fun b (Int) Bool)
(assert (b (+ a 1)))
(check-sat)
(assert (not (b 1)))
(check-sat)
(get-model)
Commit: 1bdf66b
OS: Ubuntu 22.04
The text was updated successfully, but these errors were encountered: