diff --git a/src/solver/debug.ml b/src/solver/debug.ml
index 28eb46f..af35056 100644
--- 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
index 673cebb..da93baf 100644
--- 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;