projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: eebaff1) | patch
Disable constants sharing in eq engine, disable hack in theory engine. Changes to...
authorajreynol <andrew.j.reynolds@gmail.com>
Thu, 20 Nov 2014 09:56:20 +0000 (10:56 +0100)
committerajreynol <andrew.j.reynolds@gmail.com>
Thu, 20 Nov 2014 09:59:46 +0000 (10:59 +0100)
commitf70804a7159390fcb01d8c1ec208fbfd8e544fba
treea16f6ae65eda646ab5f80ef4633b3199c648d853tree
parenteebaff108e57f15cf19c78d3b9eb27ac1d90dc11commit | diff
Disable constants sharing in eq engine, disable hack in theory engine.  Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine.
src/theory/quantifiers_engine.cpp diff | blob | history
src/theory/strings/theory_strings.cpp diff | blob | history
src/theory/strings/theory_strings.h diff | blob | history
src/theory/theory_engine.cpp diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history
test/regress/regress0/bug590.smt2.expect diff | blob | history
test/regress/regress0/strings/Makefile.am diff | blob | history