From c1228fec236c82c9cd46b194c9af062143da19c4 Mon Sep 17 00:00:00 2001 From: Matt Young Date: Mon, 9 Sep 2024 01:26:55 +1000 Subject: [PATCH] smt2: fix bitwuzla invocation Bitwuzla no longer shares options in common with Boolector. It now requires "--lang smt2", and always runs incrementally by default. --- backends/smt2/smtio.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index 5fc3ab5a4..6418061ef 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)]