Fix sygus quantifier elimination preprocess for multiple functions (#5130)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Sun, 27 Sep 2020 22:29:02 +0000 (17:29 -0500)
committerGitHub <noreply@github.com>
Sun, 27 Sep 2020 22:29:02 +0000 (17:29 -0500)
commit98cdd72fca04e76eb1057d694e1dad9717351f7f
tree5f3c93c3d046f9264b9abac11260699ca8f87387
parentb52dc978f2445c6765b806119d238ca81cb8fe90
Fix sygus quantifier elimination preprocess for multiple functions (#5130)

The option --sygus-qe-preproc performs quantifier elimination to coerce certain synthesis conjectures to be single invocation. This technique was broken when multiple synthesis functions were present. This fixes the issue and adds a regression where --sygus-qe-preproc enables a benchmark to be quickly solved.
src/theory/quantifiers/sygus/synth_engine.cpp
test/regress/CMakeLists.txt
test/regress/regress1/sygus/replicate-mod.sy [new file with mode: 0644]