diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-14 21:28:57 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-14 21:28:57 -0500 |
commit | 4fb65ae4d0018dc01fe79df8bbf7f3ec0ff583b9 (patch) | |
tree | 8237d54731d6c0190cd2c56b2b594a6f126c3485 /src/preprocessing/assertion_pipeline.h | |
parent | be6719144c88921fa39823976376961fe03f17a7 (diff) |
Fix combinations of cegqi and non-standard triggers (#4271)
Counterexample-guided instantiation may produce quantified formulas with INST_CONSTANT nodes, which are also used as patterns for non-standard triggers for E-matching. This fixes a few combinations that were problematic.
Fixes #4250, fixes #4254, fixes #4269 and fixes #4281.
Diffstat (limited to 'src/preprocessing/assertion_pipeline.h')
0 files changed, 0 insertions, 0 deletions