diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index dc89b795d..8dbb047aa 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -201,10 +201,9 @@ for fn in inconstr:
                     current_states = set(["final-%d" % i for i in range(0, num_steps+1)])
                     constr_final_start = 0
                 elif len(tokens) == 2:
-                    i = int(tokens[1])
-                    assert i < 0
-                    current_states = set(["final-%d" % i for i in range(-i, num_steps+1)])
-                    constr_final_start = -i if constr_final_start is None else min(constr_final_start, -i)
+                    arg = abs(int(tokens[1]))
+                    current_states = set(["final-%d" % i for i in range(arg, num_steps+1)])
+                    constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg)
                 else:
                     assert False
                 continue
@@ -232,9 +231,8 @@ for fn in inconstr:
                 if len(tokens) == 1:
                     current_states = set(range(0, num_steps+1))
                 elif len(tokens) == 2:
-                    i = int(tokens[1])
-                    assert i < 0
-                    current_states = set(range(-i, num_steps+1))
+                    arg = abs(int(tokens[1]))
+                    current_states = set(range(arg, num_steps+1))
                 else:
                     assert False
                 continue
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 10a134711..497b72db8 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -16,7 +16,7 @@
 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 #
 
-import sys, subprocess, re
+import sys, subprocess, re, os
 from copy import deepcopy
 from select import select
 from time import time
@@ -73,7 +73,7 @@ class SmtIo:
             self.debug_print = False
             self.debug_file = None
             self.dummy_file = None
-            self.timeinfo = True
+            self.timeinfo = os.name != "nt"
             self.unroll = False
             self.noincr = False
             self.info_stmts = list()
@@ -618,7 +618,7 @@ class SmtOpts:
         self.dummy_file = None
         self.unroll = False
         self.noincr = False
-        self.timeinfo = True
+        self.timeinfo = os.name != "nt"
         self.logic = None
         self.info_stmts = list()
         self.nocomments = False
@@ -633,7 +633,7 @@ class SmtOpts:
         elif o == "--noincr":
             self.noincr = True
         elif o == "--noprogress":
-            self.timeinfo = True
+            self.timeinfo = False
         elif o == "--dump-smt2":
             self.debug_file = open(a, "w")
         elif o == "--logic":
@@ -673,6 +673,7 @@ class SmtOpts:
 
     --noprogress
         disable timer display during solving
+        (this option is set implicitly on Windows)
 
     --dump-smt2 <filename>
         write smt2 statements to file
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index 58db882d3..de85355b5 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1083,6 +1083,15 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 		did_something = true;
 	}
 
+	// check for local objects in unnamed block
+	if (type == AST_BLOCK && str.empty())
+	{
+		for (size_t i = 0; i < children.size(); i++)
+			if (children[i]->type == AST_WIRE || children[i]->type == AST_MEMORY || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM)
+				log_error("Local declaration in unnamed block at %s:%d is an unsupported SystemVerilog feature!\n",
+						children[i]->filename.c_str(), children[i]->linenum);
+	}
+
 	// transform block with name
 	if (type == AST_BLOCK && !str.empty())
 	{
@@ -1091,7 +1100,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 
 		std::vector<AstNode*> new_children;
 		for (size_t i = 0; i < children.size(); i++)
-			if (children[i]->type == AST_WIRE || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM) {
+			if (children[i]->type == AST_WIRE || children[i]->type == AST_MEMORY || children[i]->type == AST_PARAMETER || children[i]->type == AST_LOCALPARAM) {
 				children[i]->simplify(false, false, false, stage, -1, false, false);
 				current_ast_mod->children.push_back(children[i]);
 				current_scope[children[i]->str] = children[i];
@@ -1864,7 +1873,8 @@ skip_dynamic_range_lvalue_expansion:;
 			if (str == "\\$ln" || str == "\\$log10" || str == "\\$exp" || str == "\\$sqrt" || str == "\\$pow" ||
 					str == "\\$floor" || str == "\\$ceil" || str == "\\$sin" || str == "\\$cos" || str == "\\$tan" ||
 					str == "\\$asin" || str == "\\$acos" || str == "\\$atan" || str == "\\$atan2" || str == "\\$hypot" ||
-					str == "\\$sinh" || str == "\\$cosh" || str == "\\$tanh" || str == "\\$asinh" || str == "\\$acosh" || str == "\\$atanh")
+					str == "\\$sinh" || str == "\\$cosh" || str == "\\$tanh" || str == "\\$asinh" || str == "\\$acosh" || str == "\\$atanh" ||
+					str == "\\$rtoi" || str == "\\$itor")
 			{
 				bool func_with_two_arguments = str == "\\$pow" || str == "\\$atan2" || str == "\\$hypot";
 				double x = 0, y = 0;
@@ -1901,29 +1911,34 @@ skip_dynamic_range_lvalue_expansion:;
 					y = children[1]->asReal(child_sign_hint);
 				}
 
-				newNode = new AstNode(AST_REALVALUE);
-				if (str == "\\$ln")         newNode->realvalue = ::log(x);
-				else if (str == "\\$log10") newNode->realvalue = ::log10(x);
-				else if (str == "\\$exp")   newNode->realvalue = ::exp(x);
-				else if (str == "\\$sqrt")  newNode->realvalue = ::sqrt(x);
-				else if (str == "\\$pow")   newNode->realvalue = ::pow(x, y);
-				else if (str == "\\$floor") newNode->realvalue = ::floor(x);
-				else if (str == "\\$ceil")  newNode->realvalue = ::ceil(x);
-				else if (str == "\\$sin")   newNode->realvalue = ::sin(x);
-				else if (str == "\\$cos")   newNode->realvalue = ::cos(x);
-				else if (str == "\\$tan")   newNode->realvalue = ::tan(x);
-				else if (str == "\\$asin")  newNode->realvalue = ::asin(x);
-				else if (str == "\\$acos")  newNode->realvalue = ::acos(x);
-				else if (str == "\\$atan")  newNode->realvalue = ::atan(x);
-				else if (str == "\\$atan2") newNode->realvalue = ::atan2(x, y);
-				else if (str == "\\$hypot") newNode->realvalue = ::hypot(x, y);
-				else if (str == "\\$sinh")  newNode->realvalue = ::sinh(x);
-				else if (str == "\\$cosh")  newNode->realvalue = ::cosh(x);
-				else if (str == "\\$tanh")  newNode->realvalue = ::tanh(x);
-				else if (str == "\\$asinh") newNode->realvalue = ::asinh(x);
-				else if (str == "\\$acosh") newNode->realvalue = ::acosh(x);
-				else if (str == "\\$atanh") newNode->realvalue = ::atanh(x);
-				else log_abort();
+				if (str == "\\$rtoi") {
+					newNode = AstNode::mkconst_int(x, true);
+				} else {
+					newNode = new AstNode(AST_REALVALUE);
+					if (str == "\\$ln")         newNode->realvalue = ::log(x);
+					else if (str == "\\$log10") newNode->realvalue = ::log10(x);
+					else if (str == "\\$exp")   newNode->realvalue = ::exp(x);
+					else if (str == "\\$sqrt")  newNode->realvalue = ::sqrt(x);
+					else if (str == "\\$pow")   newNode->realvalue = ::pow(x, y);
+					else if (str == "\\$floor") newNode->realvalue = ::floor(x);
+					else if (str == "\\$ceil")  newNode->realvalue = ::ceil(x);
+					else if (str == "\\$sin")   newNode->realvalue = ::sin(x);
+					else if (str == "\\$cos")   newNode->realvalue = ::cos(x);
+					else if (str == "\\$tan")   newNode->realvalue = ::tan(x);
+					else if (str == "\\$asin")  newNode->realvalue = ::asin(x);
+					else if (str == "\\$acos")  newNode->realvalue = ::acos(x);
+					else if (str == "\\$atan")  newNode->realvalue = ::atan(x);
+					else if (str == "\\$atan2") newNode->realvalue = ::atan2(x, y);
+					else if (str == "\\$hypot") newNode->realvalue = ::hypot(x, y);
+					else if (str == "\\$sinh")  newNode->realvalue = ::sinh(x);
+					else if (str == "\\$cosh")  newNode->realvalue = ::cosh(x);
+					else if (str == "\\$tanh")  newNode->realvalue = ::tanh(x);
+					else if (str == "\\$asinh") newNode->realvalue = ::asinh(x);
+					else if (str == "\\$acosh") newNode->realvalue = ::acosh(x);
+					else if (str == "\\$atanh") newNode->realvalue = ::atanh(x);
+					else if (str == "\\$itor")  newNode->realvalue = x;
+					else log_abort();
+				}
 				goto apply_newNode;
 			}
 
@@ -2158,7 +2173,7 @@ skip_dynamic_range_lvalue_expansion:;
 		}
 
 		for (auto child : decl->children)
-			if (child->type == AST_WIRE || child->type == AST_PARAMETER || child->type == AST_LOCALPARAM)
+			if (child->type == AST_WIRE || child->type == AST_MEMORY || child->type == AST_PARAMETER || child->type == AST_LOCALPARAM)
 			{
 				AstNode *wire = nullptr;
 
@@ -2218,7 +2233,7 @@ skip_dynamic_range_lvalue_expansion:;
 		}
 
 		for (auto child : decl->children)
-			if (child->type != AST_WIRE && child->type != AST_PARAMETER && child->type != AST_LOCALPARAM)
+			if (child->type != AST_WIRE && child->type != AST_MEMORY && child->type != AST_PARAMETER && child->type != AST_LOCALPARAM)
 			{
 				AstNode *stmt = child->clone();
 				stmt->replace_ids(prefix, replace_rules);
diff --git a/passes/cmds/check.cc b/passes/cmds/check.cc
index b3622cb19..bb8fe6856 100644
--- a/passes/cmds/check.cc
+++ b/passes/cmds/check.cc
@@ -44,6 +44,9 @@ struct CheckPass : public Pass {
 		log("When called with -noinit then this command also checks for wires which have\n");
 		log("the 'init' attribute set.\n");
 		log("\n");
+		log("When called with -initdrv then this command also checks for wires which have\n");
+		log("the 'init' attribute set and aren't driven by a FF cell type.\n");
+		log("\n");
 		log("When called with -assert then the command will produce an error if any\n");
 		log("problems are found in the current design.\n");
 		log("\n");
@@ -52,6 +55,7 @@ struct CheckPass : public Pass {
 	{
 		int counter = 0;
 		bool noinit = false;
+		bool initdrv = false;
 		bool assert_mode = false;
 
 		size_t argidx;
@@ -60,6 +64,10 @@ struct CheckPass : public Pass {
 				noinit = true;
 				continue;
 			}
+			if (args[argidx] == "-initdrv") {
+				initdrv = true;
+				continue;
+			}
 			if (args[argidx] == "-assert") {
 				assert_mode = true;
 				continue;
@@ -70,6 +78,49 @@ struct CheckPass : public Pass {
 
 		log_header(design, "Executing CHECK pass (checking for obvious problems).\n");
 
+		pool<IdString> fftypes;
+		fftypes.insert("$sr");
+		fftypes.insert("$ff");
+		fftypes.insert("$dff");
+		fftypes.insert("$dffe");
+		fftypes.insert("$dffsr");
+		fftypes.insert("$adff");
+		fftypes.insert("$dlatch");
+		fftypes.insert("$dlatchsr");
+		fftypes.insert("$_DFFE_NN_");
+		fftypes.insert("$_DFFE_NP_");
+		fftypes.insert("$_DFFE_PN_");
+		fftypes.insert("$_DFFE_PP_");
+		fftypes.insert("$_DFFSR_NNN_");
+		fftypes.insert("$_DFFSR_NNP_");
+		fftypes.insert("$_DFFSR_NPN_");
+		fftypes.insert("$_DFFSR_NPP_");
+		fftypes.insert("$_DFFSR_PNN_");
+		fftypes.insert("$_DFFSR_PNP_");
+		fftypes.insert("$_DFFSR_PPN_");
+		fftypes.insert("$_DFFSR_PPP_");
+		fftypes.insert("$_DFF_NN0_");
+		fftypes.insert("$_DFF_NN1_");
+		fftypes.insert("$_DFF_NP0_");
+		fftypes.insert("$_DFF_NP1_");
+		fftypes.insert("$_DFF_N_");
+		fftypes.insert("$_DFF_PN0_");
+		fftypes.insert("$_DFF_PN1_");
+		fftypes.insert("$_DFF_PP0_");
+		fftypes.insert("$_DFF_PP1_");
+		fftypes.insert("$_DFF_P_");
+		fftypes.insert("$_DLATCHSR_NNN_");
+		fftypes.insert("$_DLATCHSR_NNP_");
+		fftypes.insert("$_DLATCHSR_NPN_");
+		fftypes.insert("$_DLATCHSR_NPP_");
+		fftypes.insert("$_DLATCHSR_PNN_");
+		fftypes.insert("$_DLATCHSR_PNP_");
+		fftypes.insert("$_DLATCHSR_PPN_");
+		fftypes.insert("$_DLATCHSR_PPP_");
+		fftypes.insert("$_DLATCH_N_");
+		fftypes.insert("$_DLATCH_P_");
+		fftypes.insert("$_FF_");
+
 		for (auto module : design->selected_whole_modules_warn())
 		{
 			if (module->has_processes_warn())
@@ -109,6 +160,8 @@ struct CheckPass : public Pass {
 						if (bit.wire) wire_drivers_count[bit]++;
 			}
 
+			pool<SigBit> init_bits;
+
 			for (auto wire : module->wires()) {
 				if (wire->port_input) {
 					SigSpec sig = sigmap(wire);
@@ -121,9 +174,15 @@ struct CheckPass : public Pass {
 				if (wire->port_input && !wire->port_output)
 					for (auto bit : sigmap(wire))
 						if (bit.wire) wire_drivers_count[bit]++;
-				if (noinit && wire->attributes.count("\\init")) {
-					log_warning("Wire %s.%s has an unprocessed 'init' attribute.\n", log_id(module), log_id(wire));
-					counter++;
+				if (wire->attributes.count("\\init")) {
+					Const initval = wire->attributes.at("\\init");
+					for (int i = 0; i < GetSize(initval) && i < GetSize(wire); i++)
+						if (initval[i] == State::S0 || initval[i] == State::S1)
+							init_bits.insert(sigmap(SigBit(wire, i)));
+					if (noinit) {
+						log_warning("Wire %s.%s has an unprocessed 'init' attribute.\n", log_id(module), log_id(wire));
+						counter++;
+					}
 				}
 			}
 
@@ -150,6 +209,26 @@ struct CheckPass : public Pass {
 				log_warning("%s", message.c_str());
 				counter++;
 			}
+
+			if (initdrv)
+			{
+				for (auto cell : module->cells())
+				{
+					if (fftypes.count(cell->type) == 0)
+						continue;
+
+					for (auto bit : sigmap(cell->getPort("\\Q")))
+						init_bits.erase(bit);
+				}
+
+				SigSpec init_sig(init_bits);
+				init_sig.sort_and_unify();
+
+				for (auto chunk : init_sig.chunks()) {
+					log_warning("Wire %s.%s has 'init' attribute and is not driven by an FF cell.\n", log_id(module), log_signal(chunk));
+					counter++;
+				}
+			}
 		}
 
 		log("found and reported %d problems.\n", counter);
diff --git a/tests/simple/arraycells.v b/tests/simple/arraycells.v
index 704ca3fda..fd85a1195 100644
--- a/tests/simple/arraycells.v
+++ b/tests/simple/arraycells.v
@@ -2,7 +2,7 @@
 module array_test001(a, b, c, y);
 	input a;
 	input [31:0] b, c;
-	input [31:0] y;
+	output [31:0] y;
 
 	aoi12 p [31:0] (a, b, c, y);
 endmodule