Hi,
For this formula
(set-logic QF_LRA)
(assert (= (/ 0.0 0.0) (/ (/ 0.0 0.0) 0.0)))
(assert (not (= (/ 0.0 0.0) (/ (/ (/ 0.0 0.0) 0.0) 0.0))))
(check-sat)
Z3 reports sat, but throws out an error when model_validate is on:
(error "line 4 column 10: an invalid model was generated")
CVC4 reports unsat on this formula.
For this similar formula in Int logic:
(set-logic QF_LIA)
(assert (= (div 0 0) (div (div 0 0) 0)))
(assert (not (= (div 0 0) (div (div (div 0 0) 0) 0))))
(check-sat)
Z3 also reports sat, while CVC4 reports unsat.
When model_validate is on, z3 will also throw out the same error.
OS: Ubuntu 18.04
Revision: e2b6b12
Hi,
For this formula
Z3 reports
sat, but throws out an error when model_validate is on:CVC4 reports
unsaton this formula.For this similar formula in Int logic:
Z3 also reports
sat, while CVC4 reportsunsat.When model_validate is on, z3 will also throw out the same error.
OS: Ubuntu 18.04
Revision: e2b6b12