diff --git a/regression/solver-hardness/guards/main.c b/regression/solver-hardness/guards/main.c
new file mode 100644
index 00000000000..8152c2d0ab4
--- /dev/null
+++ b/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;
+}
diff --git a/regression/solver-hardness/guards/test.desc b/regression/solver-hardness/guards/test.desc
new file mode 100644
index 00000000000..6eac38ac4c8
--- /dev/null
+++ b/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.
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 8c97da8e1b1..216a3bd97df 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/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;
   }