1 files changed, 3 insertions, 1 deletions
diff --git a/examples/smtbmc/demo1.v b/examples/smtbmc/demo1.v
index b1e505bdd..323e6c29c 100644
--- a/examples/smtbmc/demo1.v
+++ b/examples/smtbmc/demo1.v
@@ -6,10 +6,12 @@ module demo1(input clk, input addtwo, output iseven);
 
 	always @(posedge clk)
 		cnt = (iseven ? cnt == 10 : cnt == 11) ? 0 : next_cnt;
-	
+
+`ifdef FORMAL
 	assert property (cnt != 15);
 	initial assume (!cnt[3] && !cnt[0]);
 	// initial predict ((iseven && addtwo) || cnt == 9);
+`endif
 endmodule
 
 module inc(input addtwo, output iseven, input [3:0] a, output [3:0] y);