diff --git a/docs/examples/multiclk/dpmem.sv b/docs/examples/multiclk/dpmem.sv
index 87e4f61..4a920e4 100644
--- a/docs/examples/multiclk/dpmem.sv
+++ b/docs/examples/multiclk/dpmem.sv
@@ -47,9 +47,9 @@ module top (
 	(* gclk *) reg gclk;
 
 	always @(posedge gclk) begin
-		assume ($stable(rc) || $stable(wc));
-
 		if (!init) begin
+			assume ($stable(rc) || $stable(wc));
+
 			if ($rose(rc) && shadow_valid && shadow_addr == $past(ra)) begin
 				assert (shadow_data == rd);
 			end
diff --git a/docs/source/install.rst b/docs/source/install.rst
index 418a0c5..4110d63 100644
--- a/docs/source/install.rst
+++ b/docs/source/install.rst
@@ -117,3 +117,6 @@ Boolector
   http://fmv.jku.at/boolector/
 
   https://github.com/boolector/boolector
+
+  To use the ``btor`` engine you additionally need a newer version of btorsim
+  than the boolector setup script builds: https://github.com/boolector/btor2tools
diff --git a/tests/unsorted/floor_divmod.sby b/tests/unsorted/floor_divmod.sby
new file mode 100644
index 0000000..df35f8a
--- /dev/null
+++ b/tests/unsorted/floor_divmod.sby
@@ -0,0 +1,45 @@
+[options]
+mode bmc
+depth 1
+
+[engines]
+smtbmc
+
+[script]
+read_verilog -icells -formal test.v
+prep -top top
+
+[file test.v]
+module top;
+	wire [7:0] a = $anyconst, b = $anyconst, fdiv, fmod, a2;
+	assign a2 = b * fdiv + fmod;
+
+	\$divfloor #(
+		.A_WIDTH(8),
+		.B_WIDTH(8),
+		.A_SIGNED(1),
+		.B_SIGNED(1),
+		.Y_WIDTH(8),
+	) fdiv_m (
+		.A(a),
+		.B(b),
+		.Y(fdiv)
+	);
+
+	\$modfloor #(
+		.A_WIDTH(8),
+		.B_WIDTH(8),
+		.A_SIGNED(1),
+		.B_SIGNED(1),
+		.Y_WIDTH(8),
+	) fmod_m (
+		.A(a),
+		.B(b),
+		.Y(fmod)
+	);
+
+	always @* begin
+		assume(b != 0);
+		assert(a == a2);
+	end
+endmodule