fix(bolero-kani): use cover instead of assume

camshaft · Sep 28, 2023 · ad7dd53 · ad7dd53
1 parent 8d84647
commit ad7dd53
Showing 1 changed file with 7 additions and 2 deletions.
diff --git a/lib/bolero-kani/src/lib.rs b/lib/bolero-kani/src/lib.rs
@@ -51,8 +51,13 @@ pub mod lib {
             let mut input = KaniInput { options };
             match test.test(&mut input) {
                 Ok(was_valid) => {
-                    // make sure the input that we generated was valid
-                    kani::assume(was_valid);
+                    // show if the generator was satisfiable
+                    // TODO fail the harness if it's not: https://github.com/model-checking/kani/issues/2792
+                    #[cfg(kani)]
+                    kani::cover!(
+                        was_valid,
+                        "the generator should produce at least one valid value"
+                    );
                 }
                 Err(_) => {
                     panic!("test failed");