projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f6ba348) | patch
Do not use sygus evaluation functions in sygus-inst (#8185)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 1 Mar 2022 20:46:56 +0000 (14:46 -0600)
committerGitHub <noreply@github.com>
Tue, 1 Mar 2022 20:46:56 +0000 (20:46 +0000)
commit2b62f6384a550ee961455e6b354e615cb134411c
tree7fbb533019875afb5c3cbe75e515a3262e857d6btree
parentf6ba348d9de2109fa840464c4705944f81710a10commit | diff
Do not use sygus evaluation functions in sygus-inst (#8185)

This simplification was realized while we were writing the paper.

This should avoid spurious check-model failures when using sygus-inst.
src/theory/quantifiers/sygus_inst.cpp diff | blob | history