Allow choosing a non-default solver in assertFormal

It seems that small changes can dramatically affect the speed of the
default solver (yices2), while z3 is unaffected.

Let's use the one that gives the best results.

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"))
         )