Hi,
For this formula:
(assert (exists ((a Real)) (>= (* (to_real (to_int a)) (/ 0 a)) 0)))
(check-sat)
(check-sat-using horn)
Z3 throws out a Failed to verify:
[902] % z3 small.smt2
sat
Failed to verify: lemma->get_pob()->pt().check_inductive(lemma->level(), cube, uses_level, lemma->weakness())
[903] %
[903] % cat small.smt2
(assert (exists ((a Real)) (>= (* (to_real (to_int a)) (/ 0 a)) 0)))
(check-sat)
(check-sat-using horn)
[904] %
OS: Ubuntu 18.04
Commit: 5c9fd90
Hi,
For this formula:
Z3 throws out a Failed to verify:
OS: Ubuntu 18.04
Commit: 5c9fd90