From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 22 Nov 2018 16:08:28 +0000 (+0100)
Subject: Add "smtbmc ... -- ..." feature (for "raw" smtbmc options)
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4eb91d5b883f05f6c2c4f655315ce5b16a724a44;p=SymbiYosys.git

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 5143fd8..26232a9 100644
--- 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 ec83c27..38bde62 100644
--- 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"]