Add "smtbmc ... -- ..." feature (for "raw" smtbmc options)

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/docs/source/reference.rst b/docs/source/reference.rst
index 5143fd86028af8a5ef423a8000f7eea5d18abefc..26232a962e6e3169897f3c69440ff6520a20d11e 100644 (file)
--- a/docs/source/reference.rst
+++ b/docs/source/reference.rst
@@ -241,6 +241,8 @@ The following solvers are currently supported by ``yosys-smtbmc``:
   * mathsat
   * cvc4
 
+Any additional options after ``--`` are passed to ``yosys-smtbmc`` as-is.
+
 ``aiger`` engine
 ~~~~~~~~~~~~~~~~
 

diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py
index ec83c2791584c7ad2e04faa907338d944e3f0e77..38bde6266d1234191c0ba98ca91f8dd0e008732b 100644 (file)
--- a/sbysrc/sby_engine_smtbmc.py
+++ b/sbysrc/sby_engine_smtbmc.py
@@ -67,10 +67,17 @@ def run(mode, job, engine_idx, engine):
         else:
             job.error("Invalid smtbmc options %s." % o)
 
+    xtra_opts = False
     for i, a in enumerate(args):
         if i == 0 and a == "z3" and unroll_opt is None:
                 unroll_opt = False
-        smtbmc_opts += ["-s" if i == 0 else "-S", a]
+        if a == "--":
+            xtra_opts = True
+            continue
+        if xtra_opts:
+            smtbmc_opts.append(a)
+        else:
+            smtbmc_opts += ["-s" if i == 0 else "-S", a]
 
     if presat_opt:
         smtbmc_opts += ["--presat"]