diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
index d9be4151..567dde14 100644
--- a/examples/smtbmc/demo1.v
+++ b/examples/smtbmc/demo1.v
@@ -9,7 +9,7 @@ module demo1(input clk, input addtwo, output iseven);
 
 `ifdef FORMAL
 	assert property (cnt != 15);
-	initial assume (!cnt[3] && !cnt[0]);
+	initial assume (!cnt[2]);
 `endif
 endmodule