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
[671] % z3release model_validate=true small.smt2
sat
(error "line 13 column 10: an invalid model was generated")
(
(define-fun e () Int
0)
(define-fun g () Int
17)
(define-fun d () Int
28)
(define-fun f () Int
0)
(define-fun a () Int
1)
(define-fun b () Int
27)
(define-fun c () Bool
false)
)
[672] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Bool)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(assert (<= 0 a 18))
(assert (<= 0 e 1))
(assert (<= 0 f 1 b 32 (* d g)))
(assert (= (- d a b) 0 (- a 1 (* 3 f))))
(assert (or c (< a (+ e (* 3 f)))))
(check-sat)
(get-model)
The text was updated successfully, but these errors were encountered:
Commit: 97b66d1
OS: Ubuntu 18.04
The text was updated successfully, but these errors were encountered: