Docs: Add an FAQ section (rust-lang#2250)

docs/src/SUMMARY.md

@@ -40,3 +40,7 @@
   - [Overrides](./overrides.md)
 
 - [Crates Documentation](./crates/index.md)
+
+---
+
+- [FAQ](./faq.md)

docs/src/faq.md

@@ -0,0 +1,59 @@
+# FAQs
+
+This section collects frequently asked questions about Kani.
+Please consider [opening an issue](https://github.com/model-checking/kani/issues/new/choose) if you have a question that would like to see here.
+
+## Questions
+
+<details>
+<summary>Kani doesn't fail after <code>kani::assume(false)</code>. Why?</summary>
+</br>
+
+`kani::assume(false)` (or `kani::assume(cond)` where `cond` is a condition that results in `false` in the context of the program), won't cause errors in Kani.
+Instead, such an assumption has the effect of blocking all the symbolic execution paths from the assumption.
+Therefore, all checks after the assumption should appear as [`UNREACHABLE`](#../../verification-results.md).
+That's the expected behavior for `kani::assume(false)` in Kani.
+
+If you didn't expect certain checks in a harness to be `UNREACHABLE`, we recommend using the [`kani::cover` macro](#../../verification-results.md#cover-property-results) to determine what conditions are possible in case you've over-constrained the harness.
+</details>
+
+<details>
+<summary>I implemented the <code>kani::Arbitrary</code> trait for a type that's not from my crate, and got the error
+<code>only traits defined in the current crate can be implemented for types defined outside of the crate</code>.
+What does this mean? What can I do?</summary>
+</br>
+
+This error is due to a violation of Rust's orphan rules for trait implementations, which are explained [here](https://doc.rust-lang.org/error_codes/E0117.html).
+In that case, you'll need to write a function that builds an object from non-deterministic variables.
+Inside this function you would simply return an arbitrary value by generating arbitrary values for its components.
+
+For example, let's assume the type you're working with is this enum:
+
+```rust
+#[derive(Copy, Clone)]
+pub enum Rating {
+    One,
+    Two,
+    Three,
+}
+```
+
+Then, you can match on a non-deterministic integer (supplied by `kani::any`) to return non-deterministic `Rating` variants:
+
+```rust
+    pub fn any_rating() -> Rating {
+        match kani::any() {
+            0 => Rating::One,
+            1 => Rating::Two,
+            _ => Rating::Three,
+        }
+    }
+```
+
+More details about this option, which also useful in other cases, can be found [here](https://model-checking.github.io/kani/tutorial-nondeterministic-variables.html#custom-nondeterministic-types).
+
+If the type comes from `std` (Rust's standard library), you can [open a request](https://github.com/model-checking/kani/issues/new?assignees=&labels=%5BC%5D+Feature+%2F+Enhancement&template=feature_request.md&title=) for adding `Arbitrary` implementations to the Kani library.
+Otherwise, there are more involved options to consider:
+ 1. Importing a copy of the external crate that defines the type, then implement `Arbitrary` there.
+ 2. Contributing the `Arbitrary` implementation to the external crate that defines the type.
+</details>