1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp
index 36208ff8d..7e50dad87 100644
--- a/src/theory/arith/dio_solver.cpp
+++ b/src/theory/arith/dio_solver.cpp
@@ -145,6 +145,8 @@ void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
     return;
   }
 
+
+
   uint32_t length = sp.maxLength();
   if(length > d_maxInputCoefficientLength){
     d_maxInputCoefficientLength = length;
@@ -155,7 +157,10 @@ void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
   //Variable proofVariable(makeIntegerVariable());
 
   TrailIndex posInTrail = d_trail.size();
-  d_trail.push_back(Constraint(sp,Polynomial(Monomial(VarList(proofVariable)))));
+  Debug("dio::pushInputConstraint") << "pushInputConstraint @ " << posInTrail
+                                    << " " << eq.getNode()
+                                    << " " << reason << endl;
+  d_trail.push_back(Constraint(sp,Polynomial::mkPolynomial(proofVariable)));
 
   size_t posInConstraintList = d_inputConstraints.size();
   d_inputConstraints.push_back(InputConstraint(reason, posInTrail));