This issue is due to a bug in z3.
Description
When instantiating a quantifier, z3 will substitute all quantified variables with the expressions they were instantiated with to create a resulting boolean body. However, before walking this expression to add new terms to the egraph, z3 rewrites the body using equalities. This is not logged anywhere: the new enodes we blame with an instantiation are already the rewritten terms. We would like to know which equalities were used for rewriting so that we can blame them.
Hack fix
Proof logging must be enabled! With proof logging (i.e. proof=true z3 flag) enabled, we get the proof for the instantiation from which we can extract the post-rewrite body. We then walk the general body of the quantifier (with free vars) and the instantiated post-rewrite body (without free vars) and explain discrepancies as equalities which must have been used.
This issue is due to a bug in z3.
Description
When instantiating a quantifier, z3 will substitute all quantified variables with the expressions they were instantiated with to create a resulting boolean body. However, before walking this expression to add new terms to the egraph, z3 rewrites the body using equalities. This is not logged anywhere: the new enodes we blame with an instantiation are already the rewritten terms. We would like to know which equalities were used for rewriting so that we can blame them.
Hack fix
Proof logging must be enabled! With proof logging (i.e.
proof=truez3 flag) enabled, we get the proof for the instantiation from which we can extract the post-rewrite body. We then walk the general body of the quantifier (with free vars) and the instantiated post-rewrite body (without free vars) and explain discrepancies as equalities which must have been used.