% z3-0ee7918 bug.smt2
Verification of 69 74 -70 failed
ASSERTION VIOLATION
File: ../src/sat/sat_drat.cpp
Line: 471
false
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
% cat bug.smt2
(set-option :sat.xor.solver true)
(set-option :sat.drat.check_unsat true)
(declare-fun a () Int)
(declare-fun b () Int)
(assert (and (not (and (= (+ (* (* b a))) 0))) (>= a 0)))
(check-sat)