Merge remote-tracking branch 'upstream/master'

3 files changed, 26 insertions, 9 deletions

diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index dce82f01a..92941d4cf 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -3,14 +3,30 @@ OBJS += backends/smt2/smt2.o
 
 ifneq ($(CONFIG),mxe)
 ifneq ($(CONFIG),emcc)
+
+# MSYS targets support yosys-smtbmc, but require a launcher script
+ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
+TARGETS += yosys-smtbmc.exe yosys-smtbmc-script.py
+# Needed to find the Python interpreter for yosys-smtbmc scripts.
+# Override if necessary, it is only used for msys2 targets.
+PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
+
+yosys-smtbmc-script.py: backends/smt2/smtbmc.py
+	$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' \
+		-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
+
+yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
+	$(P) gcc -DGUI=0 -O -s -o $@ $<
+# Other targets
+else
 TARGETS += yosys-smtbmc
 
 yosys-smtbmc: backends/smt2/smtbmc.py
 	$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/yosys/python3"]]|;' < $< > $@.new
 	$(Q) chmod +x $@.new
 	$(Q) mv $@.new $@
+endif
 
 $(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
 endif
 endif
-
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 7f3cc94ca..688535f33 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -416,6 +416,7 @@ struct Smt2Worker
 		for (char ch : expr) {
 			if (ch == 'A') processed_expr += get_bv(sig_a);
 			else if (ch == 'B') processed_expr += get_bv(sig_b);
+			else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B"));
 			else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
 			else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
 			else processed_expr += ch;
@@ -554,7 +555,7 @@ struct Smt2Worker
 
 			if (cell->type.in("$shift", "$shiftx")) {
 				if (cell->getParam("\\B_SIGNED").as_bool()) {
-					return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) "
+					return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
 							"(bvlshr A B) (bvlshr A (bvneg B)))",
 							GetSize(cell->getPort("\\B")), 0), 's');
 				} else {
@@ -887,8 +888,8 @@ struct Smt2Worker
 
 				string name_a = get_bool(cell->getPort("\\A"));
 				string name_en = get_bool(cell->getPort("\\EN"));
-				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id,
-						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
+				string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\src").decode_string() : get_id(cell);
+				decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str()));
 
 				if (cell->type == "$cover")
 					decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 94a5e2da0..445a42e0d 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -1484,11 +1484,11 @@ else:  # not tempind, covermode
                             smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
                             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
                             smt_assert_consequent(get_constr_expr(constr_assumes, i))
-                    print_msg("Re-solving with appended steps..")
-                    if smt_check_sat() == "unsat":
-                        print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
-                        retstatus = False
-                        break
+                        print_msg("Re-solving with appended steps..")
+                        if smt_check_sat() == "unsat":
+                            print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
+                            retstatus = False
+                            break
                     print_anyconsts(step)
                     for i in range(step, last_check_step+1):
                         print_failed_asserts(i)