From ebcbc06951ae111f38c638919e069110a9ef226b Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 22 Jun 2026 08:40:16 +0200 Subject: [PATCH] smtbmc: support latest bitwuzla --- backends/smt2/smtio.py | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 2bc7daddc..b7897fa99 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,29 @@ class SmtIo: print('timeout option is not supported for %s.' % self.solver) sys.exit(1) + if self.solver == "bitwuzla": + try: + help_text = subprocess.check_output([self.solver, "--help"], text=True) + except FileNotFoundError: + print("%s SMT Solver '%s' not found in path." % (self.timestamp(), self.solver), flush=True) + sys.exit(1) + if "--lang" in help_text: + self.popen_vargs = [self.solver, '--lang', 'smt2'] + self.solver_opts + self.unroll = True + if self.timeout != 0: + self.popen_vargs.append('--time-limit') + self.popen_vargs.append('%d000' % self.timeout) + else: + # Versions before 0.3 + if self.noincr: + self.popen_vargs = [self.solver, '--smt2'] + self.solver_opts + else: + self.popen_vargs = [self.solver, '--smt2', '-i'] + self.solver_opts + self.unroll = True + 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)]