Better debug information in string refinement

Author: romainbrenguier

src/solvers/refinement/string_refinement.cpp

@@ -1145,22 +1145,22 @@ bool string_refinementt::check_axioms()
 
     exprt negaxiom=negation_of_constraint(axiom_in_model);
 
-    debug() << "  - axiom:\n"
-            << "     " << from_expr(ns, "", axiom) << eom;
-    debug() << "  - axiom_in_model:\n"
-            << "     " << from_expr(ns, "", axiom_in_model) << eom;
-    debug() << "  - negated_axiom:\n"
-            << "     " << from_expr(ns, "", negaxiom) << eom;
+    debug() << "  "<< i << ".\n"
+            << "    - axiom:\n"
+            << "       " << from_expr(ns, "", axiom) << eom;
+    debug() << "    - axiom_in_model:\n"
+            << "       " << from_expr(ns, "", axiom_in_model) << eom;
+    debug() << "    - negated_axiom:\n"
+            << "       " << from_expr(ns, "", negaxiom) << eom;
 
     exprt with_concretized_arrays=concretize_arrays_in_expression(
       negaxiom, generator.max_string_length);
-    debug() << "  - negated_axiom_with_concretized_array_access:\n"
-            << "     " << from_expr(ns, "", with_concretized_arrays) << eom;
+    debug() << "    - negated_axiom_with_concretized_array_access:\n"
+            << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
 
     substitute_array_access(with_concretized_arrays);
-    debug() << "  - negated_axiom_without_array_access:\n"
-            << "     " << from_expr(ns, "", with_concretized_arrays) << eom;
-
+    debug() << "    - negated_axiom_without_array_access:\n"
+            << "       " << from_expr(ns, "", with_concretized_arrays) << eom;
     exprt witness;
 
     bool is_sat=is_axiom_sat(with_concretized_arrays, univ_var, witness);