fix(explorer): no more 'None' assignments crashing the executor in annotation mode

symbolic-explorer/driver/SymbolicStorage.py

@@ -55,6 +55,35 @@ def register_vars(self, sym_vars: [str], indices: [int] = None) -> None:
             self.vars[int(v.idx)] = v
             logger.info(f'[EXPLORER] Registered symbolic variable {v.dType.name}_{v.idx}')
 
+    def register_inputs(self, inputs) -> None:
+        """Register symbolic variables from the inputs recorded in a trace.
+
+        Unlike register_vars(), this keeps the concrete value observed during the
+        execution as fallback and uses the variable's real DSE index (parsed from
+        its name). If the solver's model omits a variable (e.g. it is unconstrained
+        on the solved path), the fallback value is used instead of emitting a
+        literal 'None' assignment, which would crash the executor.
+        Mirrors svcomp/SymbolicStorage.register_vars().
+
+        Args:
+            inputs: List of data.trace.Input objects (e.g. a branch node's inputs).
+        """
+        for input in inputs:
+            dtype, _, idx = input.name.rpartition('_')
+            if not idx.isdigit():
+                # Auxiliary inputs such as array-length variables ("[I_0_length")
+                # are not assignable and carry no DSE index.
+                logger.debug(f'[EXPLORER] Skipping auxiliary input {input.name}')
+                continue
+            try:
+                v = SymbolicVar(dtype=DataTypes(dtype), idx=int(idx))
+            except ValueError:
+                logger.warning(f'[EXPLORER] Skipping input {input.name} with unknown type {dtype}')
+                continue
+            v.value = input.value
+            self.vars[v.idx] = v
+            logger.info(f'[EXPLORER] Registered symbolic variable {v.dType.name}_{v.idx} (trace value: {v.value})')
+
     def init_values(self):
         for var in self.vars.values():
             match var.dType:

symbolic-explorer/driver/TargetDriver.py

@@ -70,6 +70,8 @@ def build_command(self, mem: int = 32) -> [str]:
         # Add symbolic value assignments (if we have them)
         for var in self.sym_storage.vars.values():
             val = var.newValue if var.newValue is not None else var.value
+            if val is None:
+                continue  # no known value; the executor keeps the target's original value
             # Use swat.assignment prefix (read by Intrinsics.retrieveAssignments())
             cmd.insert(1, f'-Dswat.assignment.{var.dType.value}_{var.idx}={val}')
 
@@ -95,6 +97,12 @@ def add_values(self, cmd: [str]) -> [str]:
             else:
                 val = var.newValue
                 var.value = var.newValue
+            if val is None:
+                # Neither a solver value nor a concrete fallback is known; skipping the
+                # assignment lets the executor keep the target's original value instead
+                # of crashing on parsing a literal 'None'.
+                logger.error(f'[EXPLORER] No value known for {var.dType.value}_{var.idx}, skipping assignment')
+                continue
             if self.args.mode == "args":
                 cmd.append(f'{val}')
             else:
@@ -200,7 +208,7 @@ def retrieve_solution(self):
 
         sol_viz = [f'{key}: {val["plain_value"]}' for key, val in sol.items()]
         logger.info(f'[EXPLORER] Found new solution: {sol_viz}')
-        self.sym_storage.register_vars([var.name.split('_')[0] for var in symbolic_vars])
+        self.sym_storage.register_inputs(symbolic_vars)
         self.sym_storage.store_solution(sol)
         return Action.SYMBOLICNEXT