(purify-arith aufnira) Model validation failure on valid model on NIA formula

[muchang]

Hi,
For this case, Z3 gives an invalid model error on a valid model:

[748] % z3 model_validate=true small.smt2
sat
sat
[749] % z3 smt.string_solver=z3str3 model_validate=true small.smt2
sat
sat
(error "line 11 column 44: an invalid model was generated")
[750] % 
[750] % cat small.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(assert (forall ((f Int)) (not (= (div a e) (mod c f) d))))
(assert (= b (mod f g)))
(check-sat)
(check-sat-using (then purify-arith aufnira))
[751] %

OS: Ubuntu 18.04
Commit: e525543

[NikolajBjorner]

this doesn't mention strings, so bug is orthogonal to z3str3

[NikolajBjorner]

@levnach could you check it out?

[levnach]

It does not repro in f2d3160.
./z3 ~/Dropbox/smts/4388.smt2 smt.string_solver=z3str model_validate=true
unknown
unknown
cat ~/Dropbox/smts/4388.smt2
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(assert (forall ((f Int)) (not (= (div a e) (mod c f) d))))
(assert (= b (mod f g)))
(check-sat)
(check-sat-using (then purify-arith aufnira))
Compilation finished at Wed May 20 11:14:29