fix bug

diff --git a/src/Encoders/polarityassignment.cc b/src/Encoders/polarityassignment.cc
index 77d2a060c355c11474027a69f02da7e21bc63391..bf787ea3960b33d16fb90a01aa46fb16e1eed468 100644 (file)
--- a/src/Encoders/polarityassignment.cc
+++ b/src/Encoders/polarityassignment.cc
@@ -35,8 +35,10 @@ void computePolarityAndBooleanValue(Boolean *This) {
 }
 
 void computePredicatePolarityAndBooleanValue(BooleanPredicate *This) {
-       updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
-       computePolarityAndBooleanValue(This->undefStatus);
+       if (This->undefStatus != NULL) {
+               updatePolarity(This->undefStatus, P_BOTHTRUEFALSE);
+               computePolarityAndBooleanValue(This->undefStatus);
+       }
 }
 
 void computeLogicOpPolarityAndBooleanValue(BooleanLogic *This) {

diff --git a/src/Test/buildconstraintstest.cc b/src/Test/buildconstraintstest.cc
index af28c499ade623618fb808c787c0ef0c805cf59c..71cb211113a85eedb32670698a2356c3ebffb203 100644 (file)
--- a/src/Test/buildconstraintstest.cc
+++ b/src/Test/buildconstraintstest.cc
@@ -49,7 +49,7 @@ int main(int numargs, char **argv) {
        Predicate *equal2 = solver->createPredicateOperator(EQUALS, domain2, 2);
        Element *inputs2 [] = {e4, e3};
        Boolean *pred = solver->applyPredicate(equal2, inputs2, 2);
-solver->       addConstraint(pred);
+       solver->addConstraint(pred);
 
        if (solver->startEncoding() == 1)
                printf("e1=%llu e2=%llu\n", solver->getElementValue(e1), solver->getElementValue(e2));