Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8663a2f68..9b0b93f78 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -173,6 +173,8 @@ Result PropEngine::checkSat(unsigned long& millis, unsigned long& resource) {
 
 Node PropEngine::getValue(TNode node) const {
   Assert(node.getType().isBoolean());
+  Assert(d_cnfStream->hasLiteral(node));
+
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
   SatLiteralValue v = d_satSolver->value(lit);
@@ -196,6 +198,8 @@ bool PropEngine::isTranslatedSatLiteral(TNode node) const {
 
 bool PropEngine::hasValue(TNode node, bool& value) const {
   Assert(node.getType().isBoolean());
+  Assert(d_cnfStream->hasLiteral(node));
+
   SatLiteral lit = d_cnfStream->getLiteral(node);
 
   SatLiteralValue v = d_satSolver->value(lit);