projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d3c365a) | patch
Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug fix...
authorajreynol <andrew.j.reynolds@gmail.com>
Sat, 5 Sep 2015 10:02:28 +0000 (12:02 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Sat, 5 Sep 2015 10:11:02 +0000 (12:11 +0200)
commitc38245e4f041252df011a024abe834ae7ec0ec0a
tree0452b7a998312393a2556c6cdf695af17efb91d4tree
parentd3c365a60c88e33a7d73f81484db2cff5ef69bbbcommit | diff
Fix bugs related to fmf with incremental. Reinitialize sorts on user pop, bug fix enumeration for uninitialized sorts, do not decide combined cardinality constraints that have not been allocated in user context. Fixes bug 654.
src/theory/uf/theory_uf_strong_solver.cpp diff | blob | history
src/theory/uf/theory_uf_strong_solver.h diff | blob | history
test/regress/regress0/push-pop/Makefile.am diff | blob | history
test/regress/regress0/push-pop/bug654-dd.smt2 [new file with mode: 0755] blob