projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 546d795) | patch
Answer unknown when uf-ss=no-minimal is combined with cardinality constraints from...
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Thu, 31 Aug 2017 12:26:26 +0000 (14:26 +0200)
committerGitHub <noreply@github.com>
Thu, 31 Aug 2017 12:26:26 +0000 (14:26 +0200)
commit949dc989f72c680b98a4f7c4e52616b393237b52
tree6e73970da5745515292a9192e7e5f74ca87dac66tree
parent546d795470ca7c30fc62fe9b6c7b8e5838e1eed4commit | diff
Answer unknown when uf-ss=no-minimal is combined with cardinality constraints from user input, add regressions. (#1060)
src/theory/theory_model.cpp diff | blob | history
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/fmf/Makefile.am diff | blob | history
test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 [new file with mode: 0644] blob
test/regress/regress0/fmf/no-minimal-sat.smt2 [new file with mode: 0644] blob