projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: f70804a) | patch
Revert "Disable constants sharing in eq engine, disable hack in theory engine."
authorKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 3 Dec 2014 16:38:36 +0000 (11:38 -0500)
committerKshitij Bansal <kshitij@cs.nyu.edu>
Wed, 3 Dec 2014 16:39:07 +0000 (11:39 -0500)
commit160134dc043c28308865d2b91648ba412d0749d4
treeba6977484e7368d6ccdf00273443c101c348746btree
parentf70804a7159390fcb01d8c1ec208fbfd8e544fbacommit | diff
Revert "Disable constants sharing in eq engine, disable hack in theory engine."

This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba.

In particular, it DOES NOT revert
  "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine."
which is part of the same commit.
src/theory/theory_engine.cpp diff | blob | history
src/theory/uf/equality_engine.cpp diff | blob | history