Make interpolation robust to conjectures with no shared variables (#8840)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 1 Jun 2022 12:03:04 +0000 (07:03 -0500)
committerGitHub <noreply@github.com>
Wed, 1 Jun 2022 12:03:04 +0000 (12:03 +0000)
commitbf7bd719996501a52a1d757d5c268b5ddc03dd14
treefb7e71862130065f5901d8360ad34e9ddaa59eb9
parent735cbadb137362fbc876fd056ed6ba3a9768caf1
Make interpolation robust to conjectures with no shared variables (#8840)

Fixes #8833.
src/theory/quantifiers/sygus/sygus_interpol.cpp
test/regress/cli/CMakeLists.txt
test/regress/cli/regress0/issue8833-interpol-no-shared-var.smt2 [new file with mode: 0644]