+[tasks]
+smtbmc_pass: smtbmc pass
+smtbmc_fail: smtbmc fail
+aigbmc_pass: aigbmc pass
+aigbmc_fail: aigbmc fail
+btormc_pass: btormc pass
+btormc_fail: btormc fail
+abc_pass: abc pass
+abc_fail: abc fail
+
+[options]
+mode bmc
+pass: expect pass
+fail: expect fail
+pass: depth 5
+fail: depth 6
+
+[engines]
+smtbmc: smtbmc boolector
+aigbmc: aiger aigbmc
+btormc: btor btormc
+abc: abc bmc3
+
+[script]
+read -formal top.sv
+prep -top top
+
+[file top.sv]
+module top(input clk);
+ reg [7:0] counter = 0;
+
+ always @(posedge clk) begin
+ counter <= counter + 1;
+ assert (counter < 4);
+ end
+endmodule