fixed uf proof with holes bugs

3 files changed, 12 insertions, 1 deletions

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 960f2ad62..98e43aaf0 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -103,6 +103,13 @@ void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
   Assert((unsigned)clause.size() == sat_clause.size());
 }
 
+void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
+                                       SatClause& sat_clause) {
+  for (int i = 0; i < clause.size(); ++i) {
+    sat_clause.push_back(toSatLiteral(clause[i]));
+  }
+  Assert((unsigned)clause.size() == sat_clause.size());
+}
 
 void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy)
 {
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index ec49b5f71..27258b3c2 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -51,7 +51,7 @@ public:
 
   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
   static void  toSatClause    (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);
-
+  static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
   void initialize(context::Context* context, TheoryProxy* theoryProxy);
 
   void addClause(SatClause& clause, bool removable);
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index ab2bcda47..8fee0d11e 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -135,6 +135,10 @@ public:
     return (size_t)d_value;
   }
 
+  uint64_t toInt() const {
+    return d_value; 
+  }
+  
   /**
    * Returns true if the literal is undefined.
    */