Hi,
For this formula:
(set-logic HORN)
(assert
(exists ((a Int))
(forall ((n Int))
(exists ((b Int))
(xor (and true) (distinct a b) (<= (- 1) n)
(exists ((bb Int))
(or (distinct (* (- 11) bb) b) (> 0 n))))))))
(check-sat)
Z3 throws out a Failed to verify:
[642] % z3 small.smt2
sat
[643] % z3 smt.ematching=false small.smt2
Failed to verify: lemma->get_pob()->pt().check_inductive(lemma->level(), cube, uses_level, lemma->weakness())
[644] %
[644] % cat small.smt2
(set-logic HORN)
(assert
(exists ((a Int))
(forall ((n Int))
(exists ((b Int))
(xor (and true) (distinct a b) (<= (- 1) n)
(exists ((bb Int))
(or (distinct (* (- 11) bb) b) (> 0 n))))))))
(check-sat)
[645] %
OS: Ubuntu 18.04
Commit: 2673807
Hi,
For this formula:
Z3 throws out a Failed to verify:
OS: Ubuntu 18.04
Commit: 2673807