Fix conflict

TDacik · Jan 13, 2025 · 8b2f5dc · 8b2f5dc
2 parents 241a792 + f5b986a
commit 8b2f5dc
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 2 deletions.
diff --git a/src/solver/debug.ml b/src/solver/debug.ml
@@ -78,10 +78,10 @@ let inductive_pred ?(suffix="") name phi =
 
 let input input =
   debug_out "input.txt" (ParserContext.show input);
-  formula ~force_name:"input" (ParserContext.get_phi input)
+  formula ~force_name:"input" (ParserContext.get_phi input);
+  SL.output_benchmark ((debug_dir ()) ^ "/input.smt2") (ParserContext.get_phi input) ~status:`Unknown
 
 let context context =
-  SL.output_benchmark ((debug_dir ()) ^ "/input.smt2") context.phi ~status:`Unknown;
   SL_graph.output_file (sl_graph_dot "") context.sl_graph;
   SL_graph.output_file (sl_graph_dot "_spatial") (SL_graph.spatial_projection context.sl_graph)
 

diff --git a/src/solver/solver.ml b/src/solver/solver.ml
@@ -96,6 +96,7 @@ let solve solver phi =
     let input = Input.add_assertion input phi in
     Input.add_vars input vars
   in
+  Debug.input input;
   let result = Engine.solve input in
   Profiler.finish ();
   Debug.result result;