$z3release model_validate=true delta.out.smt2                          
sat      
(error "line 5 column 10: an invalid model was generated")
$cat delta.out.smt2                                                                
(declare-fun a () Int)                                                             
(declare-fun b () Int)                                                             
(declare-fun c () Int)                                                             
(assert (and (= 0 (- (div 0 0) a)) (= 0 (+ b 1 b (* c (mod (* a (- 1)) 0))))))
(check-sat)