$ z3release model_validate=true bug.smt2
ASSERTION VIOLATION
File: ../src/sat/smt/pb_constraint.h
Line: 54
Failed to verify: k < 400000000
Z3 4.8.11.0
$ cat bug.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(assert
(let ((?c (< (+ (+ (* b a))) 0)))
(= 1 (- (ite (and ?c) 1073741823 0) (ite ?c 1 0)))))
(check-sat)