(ext-rewrite-quant) Refutation soundness bug in LIA

[muchang]

[766] % cvc4 -q small.smt2
sat
[767] % cvc4 -q --ext-rewrite-quant small.smt2
unsat
[768] % cat small.smt2
(define-fun f ((a Int) (b Int)) Int (ite (= b 0) 0 a))
(assert (exists ((c Int)) (distinct (f c (mod 0 0)) 0)))
(check-sat)
[769] % 

Commit: e0dfc0a

[muchang]

Another case:

[855] % cvc4 -q small.smt2
unknown
[856] % z3release small.smt2
sat
[857] % cvc4 -q --ext-rewrite-quant small.smt2
unsat
[858] % 
[858] % cat small.smt2
(declare-fun c (Int) Bool)
(define-fun d ((e Int)) Bool (forall ((a Int) (b Int)) (! true :pattern ((c a) (c b)))))
(assert (exists ((e Int)) (distinct (d e) (= (ite (= e 0) (mod 0 e) 0) 0))))
(check-sat)
[859] % 

Commit: e0dfc0a