diff --git a/docs/examples/quickstart/demo.sby b/docs/examples/quickstart/demo.sby
index 01fb2aa..0e8fdcf 100644
--- a/docs/examples/quickstart/demo.sby
+++ b/docs/examples/quickstart/demo.sby
@@ -6,8 +6,8 @@ depth 100
 smtbmc
 
 [script]
-read_verilog -formal demo.v
+read -formal demo.sv
 prep -top demo
 
 [files]
-demo.v
+demo.sv
diff --git a/docs/examples/quickstart/demo.v b/docs/examples/quickstart/demo.sv
similarity index 63%
rename from docs/examples/quickstart/demo.v
rename to docs/examples/quickstart/demo.sv
index 09044de..0184df4 100644
--- a/docs/examples/quickstart/demo.v
+++ b/docs/examples/quickstart/demo.sv
@@ -5,11 +5,15 @@ module demo (
   reg [5:0] counter = 0;
 
   always @(posedge clk) begin
-    if (counter == 15)
+    if (counter == 50)
       counter <= 0;
     else
       counter <= counter + 1;
   end
 
-  assert property (counter < 32);
+`ifdef FORMAL
+  always @(posedge clk) begin
+    assert (counter < 32);
+  end
+`endif
 endmodule
diff --git a/docs/source/quickstart.rst b/docs/source/quickstart.rst
index e722c19..2a170e8 100644
--- a/docs/source/quickstart.rst
+++ b/docs/source/quickstart.rst
@@ -129,7 +129,7 @@ First step: A simple BMC example
 
 Here is a simple example design with a safety property (assertion).
 
-.. literalinclude:: ../examples/quickstart/demo.v
+.. literalinclude:: ../examples/quickstart/demo.sv
    :language: systemverilog
 
 The property in this example is true. We'd like to verify this using a bounded
@@ -141,7 +141,7 @@ configure SymbiYosys to run a BMC for 100 cycles on the design:
 .. literalinclude:: ../examples/quickstart/demo.sby
    :language: text
 
-Simply create a text file ``demo.v`` with the example design and another text
+Simply create a text file ``demo.sv`` with the example design and another text
 file ``demo.sby`` with the SymbiYosys configuration. Then run::
 
    sby demo.sby