projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6444abb) | patch
Ensure CEGQI is applied for parametric datatypes when applicable (#5628)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 9 Dec 2020 04:08:52 +0000 (22:08 -0600)
committerGitHub <noreply@github.com>
Wed, 9 Dec 2020 04:08:52 +0000 (20:08 -0800)
commite0846857d7f0a926203695315b565b3541175525
treeee11d9f081808f194929f3700603b729dd2e1d5ctree
parent6444abbbcf5f298045c32ce3d69033b8f93a41d8commit | diff
Ensure CEGQI is applied for parametric datatypes when applicable (#5628)

Previously was a bug computing the argument types of parametric datatypes.
src/theory/quantifiers/cegqi/ceg_instantiator.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/quantifiers/cegqi-par-dt-simple.smt2 [new file with mode: 0644] blob