From b3e088edecc2ff68736737af6ffb6b6cd777a918 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung <dl@m-labs.hk>
Date: Wed, 19 Aug 2020 11:49:55 +0800
Subject: [PATCH] Add option to specify solver in nmigen.test.utils

---
 nmigen/test/utils.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/nmigen/test/utils.py b/nmigen/test/utils.py
index c3907ce..4124127 100644
--- a/nmigen/test/utils.py
+++ b/nmigen/test/utils.py
@@ -53,7 +53,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, engine="smtbmc"):
         caller, *_ = traceback.extract_stack(limit=2)
         spec_root, _ = os.path.splitext(caller.filename)
         spec_dir = os.path.dirname(spec_root)
@@ -80,7 +80,7 @@ class FHDLTestCase(unittest.TestCase):
         wait on
 
         [engines]
-        smtbmc
+        {engine}
 
         [script]
         read_ilang top.il
@@ -92,6 +92,7 @@ class FHDLTestCase(unittest.TestCase):
         """).format(
             mode=mode,
             depth=depth,
+            engine=engine,
             script=script,
             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
         )
-- 
2.30.2