From c6ee9522dfb17bb19ab5a40f58ecf668d65ac235 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 15 Aug 2015 18:07:01 +0200
Subject: More improvements in smt2-bmc scripts

---
 scripts/smt2-bmc/sync.py | 41 ++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 40 insertions(+), 1 deletion(-)

(limited to 'scripts/smt2-bmc/sync.py')

diff --git a/scripts/smt2-bmc/sync.py b/scripts/smt2-bmc/sync.py
index f01f0eb..6f35841 100644
--- a/scripts/smt2-bmc/sync.py
+++ b/scripts/smt2-bmc/sync.py
@@ -9,7 +9,46 @@ words = 0
 solver = "yices"
 allmem = False
 debug_print = False
-debug_file = open("debug.smt2", "w")
+debug_file = None
+
+def usage():
+    print("""
+python3 sync.py [options]
+
+    -s <solver>
+        set SMT solver: yices, z3, cvc4, mathsat
+        default: yices
+
+    -t <steps>
+        default: 20
+
+    -v
+        enable debug output
+
+    -d
+        write smt2 statements to debug.smt2
+""")
+    sys.exit(1)
+
+try:
+    opts, args = getopt.getopt(sys.argv[1:], "s:t:vd")
+except:
+    usage()
+
+for o, a in opts:
+    if o == "-s":
+        solver = a
+    elif o == "-t":
+        steps = int(a)
+    elif o == "-v":
+        debug_print = True
+    elif o == "-d":
+        debug_file = open("debug.smt2", "w")
+    else:
+        usage()
+
+if len(args) > 0:
+    usage()
 
 start_time = time()
 smt = smtio(solver=solver, debug_print=debug_print, debug_file=debug_file)
-- 
cgit