projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 48b1475) | patch
a bit more changes, when propagting equalities/dis-equalities don't assert them to...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Sat, 10 Dec 2011 07:02:21 +0000 (07:02 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Sat, 10 Dec 2011 07:02:21 +0000 (07:02 +0000)
commit3fd65ea9f5b5cdb2fe4b511b76abcad89e1cd71d
tree02ed170f72d4b48fe158da051e86bf1567f46469tree
parent48b147577ba6a894f8f0498c39c7e77d466b0538commit | diff
a bit more changes, when propagting equalities/dis-equalities don't assert them to theories that rewrite them to true. for example, 1 != 0 rewrites to true, so it shouldn't get propagated to arithmetic.
src/theory/theory_engine.cpp diff | blob | history