Allow choosing a non-default solver in assertFormal

[nmutil.git] / src / nmutil / formaltest.py

diff --git a/src/nmutil/formaltest.py b/src/nmutil/formaltest.py
index dca64ca493c886fd95790b35a38bd2cd3407024e..4b9b174848afa022a5708262183d66ee32da8745 100644 (file)
--- a/src/nmutil/formaltest.py
+++ b/src/nmutil/formaltest.py
@@ -52,7 +52,7 @@ class FHDLTestCase(unittest.TestCase):
         if msg is not None:
             self.assertEqual(str(warns[0].message), msg)
 
-    def assertFormal(self, spec, mode="bmc", depth=1):
+    def assertFormal(self, spec, mode="bmc", depth=1, solver=""):
         caller, *_ = traceback.extract_stack(limit=2)
         spec_root, _ = os.path.splitext(caller.filename)
         spec_dir = os.path.dirname(spec_root)
@@ -81,7 +81,7 @@ class FHDLTestCase(unittest.TestCase):
         wait on
 
         [engines]
-        smtbmc
+        smtbmc {solver}
 
         [script]
         read_ilang top.il
@@ -93,6 +93,7 @@ class FHDLTestCase(unittest.TestCase):
         """).format(
             mode=mode,
             depth=depth,
+            solver=solver,
             script=script,
             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
         )