diff options
| author | GCHQDeveloper560 <48131108+GCHQDeveloper560@users.noreply.github.com> | 2021-06-16 13:19:43 +0100 |
|---|---|---|
| committer | Marcelina Kościelnicka <mwk@0x04.net> | 2021-07-12 22:07:58 +0200 |
| commit | 4379375d899b917d3f6ed00db64ab52c35f4f004 (patch) | |
| tree | aa5d3b3708d03eab3334bc78f04c069b414168a8 /backends | |
| parent | 0565c642a0c5a1b1f7b98ab681bc24226b739f9a (diff) | |
| download | yosys-4379375d899b917d3f6ed00db64ab52c35f4f004.tar.gz yosys-4379375d899b917d3f6ed00db64ab52c35f4f004.tar.bz2 yosys-4379375d899b917d3f6ed00db64ab52c35f4f004.zip | |
Add support for the Bitwuzla solver
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smtio.py | 10 |
1 files changed, 5 insertions, 5 deletions
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> |