diff --git a/priv/cuter_solve_offline.py b/priv/cuter_solve_offline.py
index 6855a480..b86bbbd7 100755
--- a/priv/cuter_solve_offline.py
+++ b/priv/cuter_solve_offline.py
@@ -1,3 +1,4 @@
+#!/usr/bin/env python3
 # -*- coding: utf-8 -*-
 
 ##
@@ -12,71 +13,82 @@
 import cuter_print as cpt
 import cuter_global as cglb
 
-def solve(fname, n, printConstraints, withPrint):
-    # Do the initializations.
-    cglb.init()
-    erlSolver = cSMT.ErlangSMT(1)
-    # Load the trace.
-    r = cIO.JsonReader(fname, n)
-    for entry, rev in r:
-        if printConstraints:
-            cpt.print_cmd(entry, rev)
-        if cc.is_interpretable(entry):
-            erlSolver.command_toSolver(entry, rev)
-    # Load the axioms to the solver.
-    erlSolver.add_axioms()
-    # Solve the model.
-    if withPrint: print("Solving the model ...",)
-    slv = erlSolver.solve()
-    if withPrint: print(slv)
-    if cc.is_sat(slv):
-        m = erlSolver.encode_model()
-        if withPrint: print(m)
-        values = [e.value.value for e in m.model.entries]
-        return (slv, values)
-    return slv
+VERBOSE = True
+
+def solve(fname, n, printConstraints):
+  # Do the initializations.
+  cglb.init()
+  erlSolver = cSMT.ErlangSMT(1)
+  # Load the trace.
+  r = cIO.JsonReader(fname, n)
+  if printConstraints:
+    print("### TRACE")
+  all_entries = list(r)
+  for i, (entry, rev) in enumerate(all_entries):
+      if printConstraints:
+        if i == len(all_entries) - 1:
+          print("[TO BE REVERSED]", end=" ")
+        cpt.print_cmd(entry, rev)
+      if cc.is_interpretable(entry):
+        erlSolver.command_toSolver(entry, rev)
+  if printConstraints:
+    print()
+  # Load the axioms to the solver.
+  erlSolver.add_axioms()
+  # Solve the model.
+  slv = erlSolver.solve()
+  if VERBOSE:
+    print(str(slv).strip())
+  if cc.is_sat(slv):
+      m = erlSolver.encode_model()
+      if VERBOSE:
+        print(str(m).strip())
+      values = [e.value.value for e in m.model.entries]
+      return (slv, values)
+  return slv
 
 def usage():
-    print("Usage: cuter_solve_offline.py TraceFile NoOfConstraint [ OPTIONS ]")
-    print("PARAMETERS")
-    print("	TraceFile		The trace file of an execution.")
-    print("	NoOfConstraint		The cardinality of the constraint to reverse.")
-    print("OPTIONS")
-    print("	--print-constraints	Print all the commands as they are being loaded (for debugging).")
-    print("	-e Dir			Dir is the ebin.")
-    print("	-u Dir			Dir is the utest ebin.")
-    print("	--help			Display this information.")
+  print("Usage: cuter_solve_offline.py TraceFile NoOfConstraint [ OPTIONS ]")
+  print("PARAMETERS")
+  print("	TraceFile		The trace file of an execution.")
+  print("	NoOfConstraint		The cardinality of the constraint to reverse.")
+  print("OPTIONS")
+  print("	--print-constraints	Print all the commands as they are being loaded (for debugging).")
+  print("	-e Dir			Dir is the ebin.")
+  print("	-u Dir			Dir is the utest ebin.")
+  print("	--help			Display this information.")
 
 def run_tests(ebin, utestEbin):
-    fname = "logfile"
-    cmd = " ".join(["erl", "-noshell", "-pa", ebin, "-pa", utestEbin, "-eval",
-        "\"cuter_tests_lib:sample_trace_file(\\\"{}\\\")\"".format(fname), "-s", "init", "stop"])
-    subp.call(cmd, shell=True)
-    result = solve(fname, 3, False, False)
-    assert len(result), "Solver error"
-    assert cc.is_sat(result[0]), "Not SAT status"
-    assert ["1", "44"] == result[1], "Wrong model: {}".format(result[1])
-    try:
-        os.remove(fname)
-    except OSError:
-        pass
+  VERBOSE = False
+  fname = "logfile"
+  cmd = " ".join(["erl", "-noshell", "-pa", ebin, "-pa", utestEbin, "-eval",
+    "\"cuter_tests_lib:sample_trace_file(\\\"{}\\\")\"".format(fname), "-s", "init", "stop"])
+  subp.call(cmd, shell=True)
+  result = solve(fname, 3, False)
+  assert len(result), "Solver error"
+  assert cc.is_sat(result[0]), "Not SAT status"
+  assert ["1", "44"] == result[1], "Wrong model: {}".format(result[1])
+  try:
+    os.remove(fname)
+  except OSError:
+    pass
 
 if __name__ == "__main__":
-    shortOpts = "u:e:"
-    longOpts = ["print-constraints", "help"]
-    optlist, remainder = getopt.gnu_getopt(sys.argv[1:], shortOpts, longOpts)
-    printConstraints = False
-    ebin, utestEbin = None, None
-    for opt, arg in optlist:
-        if opt == "--help":
-            usage()
-            sys.exit(0)
-        elif opt == "--print-constraints":
-            printConstraints = True
-        elif opt == "-u":
-            utestEbin = arg
-        elif opt == "-e":
-            ebin = arg
-    if ebin != None or utestEbin != None:
-        sys.exit(run_tests(ebin, utestEbin))
-    solve(remainder[0], int(remainder[1]), printConstraints, True)
+  shortOpts = "u:e:"
+  longOpts = ["print-constraints", "help"]
+  optlist, remainder = getopt.gnu_getopt(sys.argv[1:], shortOpts, longOpts)
+  printConstraints = False
+  ebin, utestEbin = None, None
+  for opt, arg in optlist:
+    if opt == "--help":
+      usage()
+      sys.exit(0)
+    elif opt == "--print-constraints":
+      printConstraints = True
+    elif opt == "-u":
+      utestEbin = arg
+    elif opt == "-e":
+      ebin = arg
+  if ebin != None or utestEbin != None:
+    sys.exit(run_tests(ebin, utestEbin))
+  solve(remainder[0], int(remainder[1]), printConstraints)