From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 19 Feb 2017 21:52:27 +0000 (+0100)
Subject: Use smtbmc args for solver options
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=afeab488947d4e8af38861e35c660356832eea80;p=SymbiYosys.git

Use smtbmc args for solver options
---

diff --git a/sbysrc/demo.sby b/sbysrc/demo.sby
index c0fefc8..cfd67cc 100644
--- a/sbysrc/demo.sby
+++ b/sbysrc/demo.sby
@@ -2,11 +2,12 @@
 [options]
 mode bmc
 depth 10
+wait on
 
 [engines]
-smtbmc -s yices
-smtbmc -s boolector
-smtbmc -s z3 --nomem
+smtbmc yices
+smtbmc boolector -ack
+smtbmc --nomem z3
 abc bmc3
 
 [script]
diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index 15bcbd2..3977f2c 100644
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -25,18 +25,18 @@ def run(mode, job, engine_idx, engine):
     syn_opt = False
 
     opts, args = getopt.getopt(engine[1:], "s:", ["nomem", "syn"])
-    assert len(args) == 0
 
     for o, a in opts:
-        if o == "-s":
-            smtbmc_opts += ["-s", a]
-        elif o == "--nomem":
+        if o == "--nomem":
             nomem_opt = True
         elif o == "--syn":
             syn_opt = True
         else:
             assert False
 
+    for i, a in enumerate(args):
+        smtbmc_opts += ["-s" if i == 0 else "-S", a]
+
     model_name = "smt2"
     if syn_opt: model_name += "_syn"
     if nomem_opt: model_name += "_nomem"