add space back

4 files changed, 10 insertions, 16 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 30220fcf5..ad9d87b3e 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -640,8 +640,6 @@ header = "options/smt_options.h"
   read_only  = true
   help       = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)"
 
-
-
 [[option]]
   name       = "skeletonPreprocessing"
   category   = "undocumented"
diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp
index 3b6594d15..ec0fb2d54 100644
--- a/src/prop/cryptominisat.cpp
+++ b/src/prop/cryptominisat.cpp
@@ -73,7 +73,7 @@ CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry,
   std::vector<CMSat::Lit> clause(1);
   clause[0] = CMSat::Lit(d_true, false);
   d_solver->add_clause(clause);
-
+  
   clause[0] = CMSat::Lit(d_false, true);
   d_solver->add_clause(clause);
 }
@@ -92,7 +92,7 @@ ClauseId CryptoMinisatSolver::addXorClause(SatClause& clause,
   }
 
   ++(d_statistics.d_xorClausesAdded);
-
+  
   // ensure all sat literals have positive polarity by pushing
   // the negation on the result
   std::vector<CMSatVar> xor_clause;
@@ -114,7 +114,7 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
   }
 
   ++(d_statistics.d_clausesAdded);
-
+  
   std::vector<CMSat::Lit> internal_clause;
   toInternalClause(clause, internal_clause);
   bool res = d_solver->add_clause(internal_clause);
@@ -123,7 +123,7 @@ ClauseId CryptoMinisatSolver::addClause(SatClause& clause, bool removable){
 }
 
 bool CryptoMinisatSolver::ok() const {
-  return d_okay;
+  return d_okay; 
 }
 
 
@@ -160,7 +160,7 @@ SatValue CryptoMinisatSolver::solve(){
 
 SatValue CryptoMinisatSolver::solve(long unsigned int& resource) {
   // CMSat::SalverConf conf = d_solver->getConf();
-  Unreachable("Not sure how to set different limits for calls to solve in Cryptominisat");
+  Unreachable("Not sure how to set different limits for calls to solve in Cryptominisat"); 
   return solve();
 }
 
@@ -179,17 +179,13 @@ SatValue CryptoMinisatSolver::solve(const std::vector<SatLiteral>& assumptions)
 SatValue CryptoMinisatSolver::simp(){
   return toSatLiteralValue(d_solver->simplify());
 }
-
-  //SatValue CryptoMinisatSolver::simplifyFormula(){
-  //return toSatLiteralValue(d_solver->simplify());
-  //}
   
 SatValue CryptoMinisatSolver::value(SatLiteral l){
   const std::vector<CMSat::lbool> model = d_solver->get_model();
   CMSatVar var = l.getSatVariable();
   Assert (var < model.size());
   CMSat::lbool value = model[var];
-  return toSatLiteralValue(value);
+  return toSatLiteralValue(value); 
 }
 
 SatValue CryptoMinisatSolver::modelValue(SatLiteral l){
diff --git a/src/prop/cryptominisat.h b/src/prop/cryptominisat.h
index e68532518..e05cab485 100644
--- a/src/prop/cryptominisat.h
+++ b/src/prop/cryptominisat.h
@@ -62,7 +62,7 @@ public:
   void markUnremovable(SatLiteral lit);
 
   void interrupt() override;
-
+  
   SatValue solve() override;
   SatValue solve(long unsigned int&) override;
   SatValue solve(const std::vector<SatLiteral>& assumptions) override;
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 2aa4f7357..25b2ccc39 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -31,7 +31,7 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
-
+  
 class BitVectorProof;
 
 namespace prop {
@@ -54,7 +54,7 @@ public:
 
   /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
   virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
-
+  
   /**
    * Create a new boolean variable in the solver.
    * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
@@ -102,7 +102,7 @@ public:
 
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
-
+  
   virtual void setProofLog( BitVectorProof * bvp ) {}