From 35a6553609d8025b6b39dfc5b544d22ecb731961 Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Tue, 18 Aug 2020 16:05:36 +0800 Subject: [PATCH 1/3] Pass --nopresat flag to sby --- checks/genchecks.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checks/genchecks.py b/checks/genchecks.py index 4448115..fae2396 100644 --- a/checks/genchecks.py +++ b/checks/genchecks.py @@ -562,7 +562,7 @@ def checks_key(check): for check in checks: print("%s: %s/status" % (check, check), file=mkfile) print("%s/status:" % check, file=mkfile) - print("\t%s %s.sby" % (sbycmd, check), file=mkfile) + print("\t%s --nopresat %s.sby" % (sbycmd, check), file=mkfile) print(".PHONY: %s" % check, file=mkfile) print("Generated %d checks." % (len(consistency_checks) + len(instruction_checks))) From d9c5076885368a038484b430d5460942ea3db49a Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Tue, 18 Aug 2020 16:18:31 +0800 Subject: [PATCH 2/3] Remove --nopresat flag in checks/genchecks.py --- checks/genchecks.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checks/genchecks.py b/checks/genchecks.py index fae2396..4448115 100644 --- a/checks/genchecks.py +++ b/checks/genchecks.py @@ -562,7 +562,7 @@ def checks_key(check): for check in checks: print("%s: %s/status" % (check, check), file=mkfile) print("%s/status:" % check, file=mkfile) - print("\t%s --nopresat %s.sby" % (sbycmd, check), file=mkfile) + print("\t%s %s.sby" % (sbycmd, check), file=mkfile) print(".PHONY: %s" % check, file=mkfile) print("Generated %d checks." % (len(consistency_checks) + len(instruction_checks))) From b323abe6ae617f3288b86f7c35c529ea8478247e Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Tue, 18 Aug 2020 17:29:07 +0800 Subject: [PATCH 3/3] Add --nopresat flag to sby --- checks/genchecks.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checks/genchecks.py b/checks/genchecks.py index 4448115..7e08ee0 100644 --- a/checks/genchecks.py +++ b/checks/genchecks.py @@ -154,7 +154,7 @@ def print_hfmt(f, text, **kwargs): hargs["engine"] = "btor btormc" hargs["ilang_file"] = corename + "-hier.il" else: - hargs["engine"] = "smtbmc %s%s" % ("--dumpsmt2 " if dumpsmt2 else "", solver) + hargs["engine"] = "smtbmc --nopresat %s%s" % ("--dumpsmt2 " if dumpsmt2 else "", solver) hargs["ilang_file"] = corename + "-hier.il" def test_disabled(check):