satcheck minisat2: make all solver hardness processing conditional

There is no need to run process_clause when its output wouldn't even be
used.

Author: tautschnig

src/solvers/sat/satcheck_minisat2.cpp

@@ -140,22 +140,24 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
 
     solver->addClause_(c);
 
-    // To map clauses to lines of program code, track clause indices in the
-    // dimacs cnf output. Dimacs output is generated after processing clauses
-    // to remove duplicates and clauses that are trivially true. Here, a clause
-    // is checked to see if it can be thus eliminated. If not, add the clause
-    // index to list of clauses in solver_hardnesst::register_clause().
-    static size_t cnf_clause_index = 0;
-    bvt cnf;
-    bool clause_removed = process_clause(bv, cnf);
-
-    if(!clause_removed)
-      cnf_clause_index++;
-
     with_solver_hardness(
       [&bv, &cnf, &clause_removed](solver_hardnesst &hardness) {
+        // To map clauses to lines of program code, track clause indices in the
+        // dimacs cnf output. Dimacs output is generated after processing
+        // clauses to remove duplicates and clauses that are trivially true.
+        // Here, a clause is checked to see if it can be thus eliminated. If
+        // not, add the clause index to list of clauses in
+        // solver_hardnesst::register_clause().
+        static size_t cnf_clause_index = 0;
+        bvt cnf;
+        bool clause_removed = process_clause(bv, cnf);
+
+        if(!clause_removed)
+          cnf_clause_index++;
+
         hardness.register_clause(bv, cnf, cnf_clause_index, !clause_removed);
       });
+
     clause_counter++;
   }
   catch(const Minisat::OutOfMemoryException &)