rewriter.push_ite_arith rewriter.eq2ineq fp.xform.elim_term_ite rewriter.arith_ineq_lhs with horn Assertion violation at ../src/muz/transforms/dl_mk_elim_term_ite.cpp Line: 168

[muchang]

Hi,
For this formula:

(set-option :rewriter.push_ite_arith true)
(set-option :rewriter.eq2ineq true)
(set-option :fp.xform.elim_term_ite true)
(set-option :rewriter.arith_ineq_lhs true)
(assert
 (forall ((a Bool) (b Bool) (c Int) (d Int))
 (= d (ite (= a b) 0 (ite (= c 0) (+ c 1) c)))))
(check-sat-using horn)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/muz/transforms/dl_mk_elim_term_ite.cpp
Line: 168
!has_term_ite(fml2)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: cb13641

[agurfinkel]

comment to self: check why the assertion was failing

[NikolajBjorner]

comment to self: check why the assertion was failing

The assertion is failing in part because it is an ite where
the then and else branch have type Bool.
The blast_term_ite_tactic does not expand such subterms because it will not help the SMT solver to change these terms. The SMT solver clausifies ite formulas already and there is no point in hoisting them.
Perhaps the transformation rule should also allow such Boolean ite expressions as the potential advantages of removing ite expressions possibly for arithmetic reasoning.

[agurfinkel]

moved assert into a trace print in d53e30e