Merge pull request #7309 from tautschnig/bugfixes/6333-solver-stats

Solver stats reporting: fix expression mapping for guards

Author: tautschnig

regression/solver-hardness/guards/main.c

@@ -0,0 +1,15 @@
+int main()
+{
+  int a;
+  if(a > 0)
+  {
+    if(a > 10)
+    {
+      (void)a;
+      goto out;
+    }
+  }
+  __CPROVER_assert(a > 0, "should fail");
+out:
+  return 0;
+}

regression/solver-hardness/guards/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--write-solver-stats-to 'solver_hardness.json'
+^EXIT=10$
+^SIGNAL=0$
+^\[main.assertion.1\] line 12 should fail: FAILURE$
+^VERIFICATION FAILED$
+\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"goto_symex::\\\\guard#1 ∧ goto_symex::\\\\guard#2","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}
+--
+^warning: ignoring
+\{"GOTO":"GOTO \d+","GOTO_ID":\d+,"SAT_hardness":\{"ClauseSet":\[\d+.*\],"Clauses":[1-9]\d*,"Literals":[1-9]\d*,"Variables":[1-9]\d*},"SSA_expr":"true","Source":\{"file":"main.c","function":"main","line":"\d+","workingDirectory":".*"\}\}
+--
+"true" must not yield any clauses.

src/goto-symex/symex_target_equation.cpp

@@ -416,7 +416,9 @@ void symex_target_equationt::convert_guards(
 
       step.guard_handle = decision_procedure.handle(step.guard);
       with_solver_hardness(
-        decision_procedure, hardness_register_ssa(step_index, step));
+        decision_procedure, [step_index, &step](solver_hardnesst &hardness) {
+          hardness.register_ssa(step_index, step.guard, step.source.pc);
+        });
     }
     ++step_index;
   }