projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8d7787f) | patch
Fix sygus-inst when combined with bounded string quantifiers (#8500)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 1 Apr 2022 04:25:05 +0000 (23:25 -0500)
committerGitHub <noreply@github.com>
Fri, 1 Apr 2022 04:25:05 +0000 (04:25 +0000)
commit469de059de55ad61b4f8601d4da6020ed42e368d
treeefd65baff3d9d8cc28990d955af42ea9431a2129tree
parent8d7787f310e385056badf3580914195372ba87e4commit | diff
Fix sygus-inst when combined with bounded string quantifiers (#8500)

Strings introduces bounded quantified formulas for reasoning about extended functions. We should not process these with sygus-inst.

Fixes #8497.
src/theory/quantifiers/sygus_inst.cpp diff | blob | history
src/theory/quantifiers/sygus_inst.h diff | blob | history
test/regress/cli/CMakeLists.txt diff | blob | history
test/regress/cli/regress1/quantifiers/issue8497-syqi-str-fmf.smt2 [new file with mode: 0644] blob