Minor code refactor; update tests w/new output

runtimeverification · Jul 10, 2023 · 13c0f97 · 13c0f97
1 parent c283305
commit 13c0f97
Show file tree

Hide file tree

Showing 16 changed files with 280 additions and 238 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/foundry.py b/kevm-pyk/src/kevm_pyk/foundry.py
@@ -828,8 +828,7 @@ def foundry_get_model(
             res_lines.append('')
             res_lines.append(f'Node id: {node_id}')
             node = proof.kcfg.node(node_id)
-            model_info = print_model(node, kcfg_explore)
-            res_lines.extend(model_info)
+            res_lines.extend(print_model(node, kcfg_explore))
 
     return '\n'.join(res_lines)
 

diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -193,8 +193,7 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore) -> list[str]:
             for node in proof.pending:
                 res_lines.append('')
                 res_lines.append(f'ID: {node.id}:')
-                counterexample = print_model(node, kcfg_explore)
-                res_lines.extend(counterexample)
+                res_lines.extend(print_model(node, kcfg_explore))
         if num_failing > 0:
             res_lines.append('')
             res_lines.append('Failing nodes:')
@@ -215,8 +214,7 @@ def print_failure_info(proof: Proof, kcfg_explore: KCFGExplore) -> list[str]:
                 res_lines.append('  Path condition:')
                 res_lines += [f'    {kcfg_explore.kprint.pretty_print(proof.path_constraints(node.id))}']
 
-                counterexample = print_model(node, kcfg_explore)
-                res_lines.extend(counterexample)
+                res_lines.extend(print_model(node, kcfg_explore))
 
         res_lines.append('')
         res_lines.append(