add smtbmc_opts argument to assertFormal to allow passing more solver flags

diff --git a/src/nmutil/formaltest.py b/src/nmutil/formaltest.py
index dd2b4ae45029db82ad53b6e69c8060cd09471836..db89f9e342ad63117a4313a601803d6effae860a 100644 (file)
--- a/src/nmutil/formaltest.py
+++ b/src/nmutil/formaltest.py
@@ -26,7 +26,7 @@ class FHDLTestCase(unittest.TestCase):
         self.assertEqual(prepare_repr(repr(obj)), prepare_repr(repr_str))
 
     def assertFormal(self, spec, mode="bmc", depth=1, solver="",
-                     base_path="formal_test_temp"):
+                     base_path="formal_test_temp", smtbmc_opts="--logic=ALL"):
         path = get_test_path(self, base_path)
 
         # The sby -f switch seems not fully functional when sby is
@@ -49,7 +49,7 @@ class FHDLTestCase(unittest.TestCase):
         wait on
 
         [engines]
-        smtbmc {solver} -- -- --logic=ALL
+        smtbmc {solver} -- -- {smtbmc_opts}
 
         [script]
         read_ilang top.il
@@ -63,6 +63,7 @@ class FHDLTestCase(unittest.TestCase):
             depth=depth,
             solver=solver,
             script=script,
+            smtbmc_opts=smtbmc_opts,
             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
         )
         with subprocess.Popen([require_tool("sby"), "-d", "job"],