Fix explorer mode for basic-1 and string-literal constraints

symbolic-explorer/driver/SimpleDriver.py

@@ -60,6 +60,7 @@ def build_command(self) -> List[str]:
             f'-Dexplorer.port={self.args.port}',
             f'-javaagent:{self.args.agent}',
             f'-Djava.library.path={self.args.z3dir}',
+            '-Dsolver.mode=HTTP',
             '-ea',  # Enable assertions
         ]
 
@@ -172,8 +173,8 @@ def get_next_solution(self) -> bool:
                 # Array variables come in pairs: [I_0 (the array) and [I_0_length (the length)
                 # We only want to register the array itself, not the length
                 non_length_inputs = [inp for inp in branch.inputs if not inp.name.endswith('_length')]
-                var_types = [inp.type for inp in non_length_inputs]
-                var_indices = [int(inp.name.split('_')[-1]) for inp in non_length_inputs]
+                var_types = [inp.name.rsplit('_', 1)[0] for inp in non_length_inputs]
+                var_indices = [int(inp.name.rsplit('_', 1)[1]) for inp in non_length_inputs]
                 self.sym_storage.register_vars(var_types, var_indices)
                 self.sym_storage.store_solution(sol)
 

symbolic-explorer/parse/TraceParser.py

@@ -14,14 +14,7 @@ def parse_trace(trace: List[TraceItem], trace_id: str) -> List:
         _trace = []
         for branch in trace:
             if branch.type == "Branch":
-                sanitized_constraint = ''
-                for c in branch.constraint:
-                    if ord(c) == 34:
-                        sanitized_constraint += '\\"'
-                    elif ord(c) == 10:
-                        sanitized_constraint += ''
-                    else:
-                        sanitized_constraint += c
+                sanitized_constraint = branch.constraint.replace('\n', '')
                 _trace.append(Branch(id=branch.iid,
                                      trace_id=trace_id,
                                      has_branched=branch.branched,

targets/examples/basic-1/run.sh

@@ -23,7 +23,12 @@ echo "Running $target" in $mode mode
 # Execute based on the mode
 if [ "$mode" == "explorer" ]; then
     # Running the target from the symbolic explorer
-    python ../../../symbolic-explorer/SymbolicExplorer.py --target $target --agent ../../../symbolic-executor/lib/symbolic-executor.jar --z3dir ../../../libs/java-library-path
+    ../../../symbolic-explorer/.venv/bin/python3 ../../../symbolic-explorer/SymbolicExplorer.py \
+        --mode simple \
+        --target $target \
+        --classpath . \
+        --agent ../../../symbolic-executor/lib/symbolic-executor.jar \
+        --z3dir ../../../libs/java-library-path
 else
     # Running the target from the symbolic executor
     java \