Use smtbmc args for solver options

diff --git a/sbysrc/demo.sby b/sbysrc/demo.sby
index c0fefc89084598901f04b270eaab83d26ccff2d5..cfd67cc90f3c3b4daa9df1970795e2d118a61645 100644 (file)
--- 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 15bcbd232ca2931c3fc804b37e9f06a00538961a..3977f2c90abce23509462e30816b4fbca1d210e1 100644 (file)
--- 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"