From 88f2dbc9d903381e2ce9ab15b12495eec8f5676e Mon Sep 17 00:00:00 2001 From: bdemsky Date: Thu, 24 Aug 2017 19:24:36 -0700 Subject: [PATCH] fix bug --- src/Encoders/polarityassignment.cc | 6 ++++-- src/Test/buildconstraintstest.cc | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/Encoders/polarityassignment.cc b/src/Encoders/polarityassignment.cc index 77d2a06..bf787ea 100644 --- 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 af28c49..71cb211 100644 --- 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)); -- 2.34.1