Fix test and update doc

model-checking · Aug 2, 2023 · 5ea6ded · 5ea6ded
1 parent 2b9838f
commit 5ea6ded
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 5 deletions.
diff --git a/docs/src/reference/attributes.md b/docs/src/reference/attributes.md
@@ -203,8 +203,8 @@ VERIFICATION:- SUCCESSFUL
 This may change the verification time required to verify a harness.
 
 At present, `<solver>` can be one of:
- - `minisat` (default): [MiniSat](http://minisat.se/).
- - `cadical`: [CaDiCaL](https://github.com/arminbiere/cadical).
+ - `minisat`: [MiniSat](http://minisat.se/).
+ - `cadical` (default): [CaDiCaL](https://github.com/arminbiere/cadical).
  - `kissat`: [kissat](https://github.com/arminbiere/kissat).
  - `bin="<SAT_SOLVER_BINARY>"`: A custom solver binary, `"<SAT_SOLVER_BINARY>"`, that must be in path.
 
@@ -226,6 +226,11 @@ fn check() {
 
 Changing the solver may result in different verification times depending on the harness.
 
+Note that the default solver may vary depending on Kani's version.
+We highly recommend users to annotate their harnesses if the choice of solver
+has a major impact on performance, even if the solver used is the current
+default one.
+
 ## `#[kani::stub(<original>, <replacement>)]`
 
 **Replaces the function/method with name <original> with the function/method with name <replacement> during compilation**

diff --git a/tests/ui/concrete-playback/message-order/expected b/tests/ui/concrete-playback/message-order/expected
@@ -6,8 +6,8 @@ Concrete playback unit test for `dummy`:
 #[test]
 fn kani_concrete_playback_dummy
     let concrete_vals: Vec<Vec<u8>> = vec![
-        // 32778
-        vec![10, 128, 0, 0],
+        // 10
+        vec![10, 0, 0, 0],
     ];
     kani::concrete_playback_run(concrete_vals, dummy);
 }

diff --git a/tests/ui/concrete-playback/message-order/main.rs b/tests/ui/concrete-playback/message-order/main.rs
@@ -5,5 +5,5 @@
 
 #[kani::proof]
 fn dummy() {
-    kani::cover!(kani::any::<u32>() != 10);
+    kani::cover!(kani::any::<u32>() == 10);
 }