diff --git a/klee-examples/Cargo.toml b/klee-examples/Cargo.toml
index a9a1b2fea16b70125294315fd2d177100ca3be18..47c43251f92ed9d1bca9daf822b90ef3c18e3b79 100644
--- a/klee-examples/Cargo.toml
+++ b/klee-examples/Cargo.toml
@@ -1,5 +1,6 @@
 [package]
 name = "klee-examples"
+edition = "2018"
 version = "0.2.0"
 authors = ["Per Lindgren <per.lindgren@ltu.se>", "Jorge Aparicio <jorge@japaric.io>"]
 
@@ -48,6 +49,10 @@ path = "src/peripheral.rs"
 name = "clk"
 path = "src/clk.rs"
 
+[[bin]]
+name = "clk_simple"
+path = "src/clk_simple.rs"
+
 [profile.dev]
 incremental = false
 # lto = true
diff --git a/klee-examples/src/clk_simple.rs b/klee-examples/src/clk_simple.rs
new file mode 100644
index 0000000000000000000000000000000000000000..5c5e5d3771528d93333b30336e237f6f60466b4f
--- /dev/null
+++ b/klee-examples/src/clk_simple.rs
@@ -0,0 +1,99 @@
+//! `cargo klee` will find several paths to aborts, but only one non-abort path.
+//! This path contains a clock configuration that fulfills the requirements.
+
+#![no_std]
+#![no_main]
+
+extern crate panic_abort;
+
+use klee::{kassert, ksymbol};
+
+#[derive(Clone, Copy, Debug)]
+pub struct CFGR {
+    hse: Option<u32>,
+    hclk: Option<u32>,
+    pclk1: Option<u32>,
+    pclk2: Option<u32>,
+    sysclk: Option<u32>,
+    usbclk: bool,
+}
+
+pub struct Requirements {
+    pllsrcclk: u32,
+    sysclk: u32,
+    usbclk: bool,
+}
+
+pub struct Config {
+    pllp: u32,
+    pllm: u32,
+    plln: u32,
+    pllq: u32,
+}
+
+fn pll_check(c: Config, req: Requirements) {
+    // assertions on requirements
+    kassert!(req.pllsrcclk % 1_000_000 == 0); // Multiple of 1MHz
+    kassert!(4_000_000 <= req.pllsrcclk && req.pllsrcclk <= 26_000_000); // Multiple of 1MHz
+    kassert!(req.sysclk % 1_000_000 == 0); // Multiple of 1MHz
+
+    // Sysclk output divisor must be one of 2, 4, 6 or 8
+    // (&!1 implies even numbers)
+    kassert!(c.pllp == core::cmp::min(8, (432_000_000 / req.sysclk) & !1));
+
+    kassert!(1 < c.pllm && c.pllm < 64); // field constraint
+
+    // Oscillator input constraint in the range from 1 to 2 MHz
+    kassert!(1_000_000 <= req.pllsrcclk / c.pllm && req.pllsrcclk / c.pllm <= 2_000_000);
+
+    // Main scaler,
+    assert!(c.plln == req.sysclk * c.pllp / (req.pllsrcclk / c.pllm));
+    assert!(50 <= c.plln && c.plln <= 432); // field constraint
+
+    // Oscillator output constraint
+    let osc = (req.pllsrcclk / c.pllm) * c.plln;
+    // 100MHz <= OSC <= 432MHz
+    kassert!(100_000_000 <= osc && osc <= 432_000_000);
+
+    // compute USB clock
+    // OSC / pllq = 48Mhz
+    if req.usbclk {
+        kassert!(c.pllq == osc / 48_000_000);
+        kassert!(osc / c.pllq == 48_000_000); // soundness
+        kassert!(1 < c.pllq && c.pllq < 16); // field constraint
+    } else {
+        kassert!(c.pllq == 2); // set a valid value
+    };
+
+    // Calculate real system clock
+    let sysclk_real = osc / c.pllp;
+
+    kassert!(sysclk_real == req.sysclk);
+}
+
+#[no_mangle]
+fn main() {
+    let mut pllp: u32 = 0;
+    let mut pllm: u32 = 0;
+    let mut plln: u32 = 0;
+    let mut pllq: u32 = 0;
+    ksymbol!(&mut pllp, "pllp");
+    ksymbol!(&mut pllm, "pllm");
+    ksymbol!(&mut plln, "plln");
+    ksymbol!(&mut pllq, "pllq");
+
+    let conf = Config {
+        pllp,
+        pllm,
+        plln,
+        pllq,
+    };
+
+    let req = Requirements {
+        pllsrcclk: 8_000_000,
+        sysclk: 96_000_000,
+        usbclk: true,
+    };
+
+    pll_check(conf, req);
+}