projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e47fa13) | patch
Guard against null relevancy condition in SyGuS (#4033)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 11 Mar 2020 22:54:07 +0000 (17:54 -0500)
committerGitHub <noreply@github.com>
Wed, 11 Mar 2020 22:54:07 +0000 (17:54 -0500)
commit98178c539c4eb502d3f3c3c4f1fcf0600d229b46
tree0cb046dfae455f9936ee872e1c7671c2cb521534tree
parente47fa1305536d0e2d3c16ef2225d2b8534d5aa39commit | diff
Guard against null relevancy condition in SyGuS (#4033)

Fixes #4025.

Also makes our sygus default grammar for strings (slightly) better by including a dummy character, which is required for solving the regression added by this PR. A more robust (but unintuitive to the user) solution would be to include str.from_code( Start_Int ).
src/theory/datatypes/sygus_extension.cpp diff | blob | history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/sygus/issue4025-no-rlv-cond.smt2 [new file with mode: 0644] blob