diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 2bc7daddc..b021d0184 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -226,7 +226,7 @@ class SmtIo: print('timeout option is not supported for mathsat.') sys.exit(1) - if self.solver in ["boolector", "bitwuzla"]: + if self.solver == "boolector": if self.noincr: self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts else: @@ -236,6 +236,15 @@ class SmtIo: print('timeout option is not supported for %s.' % self.solver) sys.exit(1) + if self.solver == "bitwuzla": + self.popen_vargs = [self.solver, '--lang', 'smt2'] + self.solver_opts + self.unroll = True + # Bitwuzla always uses incremental solving + self.noincr = False + if self.timeout != 0: + print('timeout option is not supported for %s.' % self.solver) + sys.exit(1) + if self.solver == "abc": if len(self.solver_opts) > 0: self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]