From: GCHQDeveloper560 <48131108+GCHQDeveloper560@users.noreply.github.com>
Date: Wed, 16 Jun 2021 12:19:43 +0000 (+0100)
Subject: Add support for the Bitwuzla solver
X-Git-Tag: yosys-0.10~108
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4379375d899b917d3f6ed00db64ab52c35f4f004;p=yosys.git

Add support for the Bitwuzla solver
---

diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 97eb1c537..d73a875ba 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -203,14 +203,14 @@ class SmtIo:
                 print('timeout option is not supported for mathsat.')
                 sys.exit(1)
 
-        if self.solver == "boolector":
+        if self.solver in ["boolector", "bitwuzla"]:
             if self.noincr:
-                self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
+                self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts
             else:
-                self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
+                self.popen_vargs = [self.solver, '--smt2', '-i'] + self.solver_opts
             self.unroll = True
             if self.timeout != 0:
-                print('timeout option is not supported for boolector.')
+                print('timeout option is not supported for %s.' % self.solver)
                 sys.exit(1)
 
         if self.solver == "abc":
@@ -1010,7 +1010,7 @@ class SmtOpts:
     def helpmsg(self):
         return """
     -s <solver>
-        set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
+        set SMT solver: z3, yices, boolector, bitwuzla, cvc4, mathsat, dummy
         default: yices
 
     -S <opt>