don't lookup step ids when the full proof is not being logged

Author: maartenflippo

pumpkin-solver/src/engine/conflict_analysis/resolvers/resolution_resolver.rs

@@ -307,7 +307,7 @@ impl ResolutionResolver {
 
         // Log all non-initial bounds to the proof.
         if dec_level == 0 && !is_completing_proof {
-            if !assignments.is_initial_bound(predicate) {
+            if !assignments.is_initial_bound(predicate) && proof_log.is_logging_inferences() {
                 let trail_index = assignments
                     .get_trail_position(&predicate)
                     .expect("all predicates in reason are true");
@@ -317,7 +317,12 @@ impl ResolutionResolver {
                 let step_id = unit_nogood_step_ids
                     .get(&trail_entry.predicate)
                     .copied()
-                    .unwrap();
+                    .unwrap_or_else(|| {
+                        panic!(
+                            "Failed to get step id for unit clause {:?}. Available steps: {:?}",
+                            trail_entry.predicate, unit_nogood_step_ids
+                        )
+                    });
                 proof_log.add_propagation(step_id);
             }
 

pumpkin-solver/src/engine/constraint_satisfaction_solver.rs

@@ -1339,7 +1339,10 @@ impl ConstraintSatisfactionSolver {
                 if let Some(step_id) = self.unit_nogood_step_ids.get(&trail_entry.predicate) {
                     self.internal_parameters.proof_log.add_propagation(*step_id);
                 } else {
-                    unreachable!()
+                    panic!(
+                        "Failed to obtain step id for predicate {:?}. Available step ids: {:?}",
+                        trail_entry.predicate, self.unit_nogood_step_ids,
+                    );
                 }
             }
 
@@ -1464,8 +1467,8 @@ impl ConstraintSatisfactionSolver {
         )
         .is_err()
         {
-            self.log_root_propagation_to_proof(num_trail_entries, None);
             self.prepare_for_conflict_resolution();
+            self.log_root_propagation_to_proof(num_trail_entries, None);
             self.complete_proof();
             return Err(ConstraintOperationError::InfeasibleNogood);
         }