projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5f207ba) | patch
Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts.
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 22 Dec 2015 11:03:10 +0000 (12:03 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 22 Dec 2015 11:03:10 +0000 (12:03 +0100)
commitbd6a13bbb46c272561c01b7783f62ff7be091c2c
tree0fb8e93664b68b961878a9a208423aaa5e85656atree
parent5f207ba01302c3245e169bfbe2ed91ad0cd659cdcommit | diff
Bug fix for cbqi, do not use model values for terms involving non-enumerable sorts.
src/theory/quantifiers/ceg_instantiator.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.cpp diff | blob | history
src/theory/quantifiers/inst_strategy_cbqi.h diff | blob | history
src/theory/quantifiers/term_database.cpp diff | blob | history
test/regress/regress0/fmf/forall_unit_data.smt2 [new file with mode: 0755] blob