Added an FAQ about array theory in CBMC

docs/src/SUMMARY.md

@@ -27,6 +27,9 @@
   * [How does malloc work?](faq/malloc.md)
   * [How do I write a good stub?]()
   * [What do I do when CBMC won't stop?](faq/termination.md)
+
+* [Advanced Questions](advanced-questions/README.md)
+  * [Does CBMC have any support for using array-theory?](advanced-questions/array-theory.md)
 
 * [CBMC project management](management/README.md)
   * [Project planning](management/Plan-your-proof.md)
@@ -37,4 +40,4 @@
 
 * [CBMC projects](projects.md)
 
-* [CBMC resources](resources.md)
+* [CBMC resources](resources.md)

docs/src/advanced-questions/README.md

@@ -0,0 +1,8 @@
+# Advanced Questions (Infrequently asked questions)
+
+Here are answers to some questions asked by advanced CBMC users.
+Please send us any questions you have by
+[filing an issue with us](https://github.com/model-checking/cbmc-training/issues)
+on GitHub.
+
+* [Does CBMC have any support for using array-theory?](array-theory.md)

docs/src/advanced-questions/array-theory.md

@@ -0,0 +1,20 @@
+# Does CBMC have any support for using array theory?
+[Article Date: Aug 10, 2022]
+
+CBMC provides support for reasoning about arrays using array theory. (Note that we are still working with a SAT back-end here, and this does not use an SMT solver)
+A fixed length array uses CBMC's typical bit-vector representation of an array, but a variable length array uses CBMC's array theory.
+To activate CBMC's array-theory for fixed length arrays, use the following workaround.
+
+```
+unsigned long size;  // non deterministically pick the size
+ArrayElement *a = malloc(size * sizeof(ArrayElement));
+__CPROVER_assume(size == MAX_SIZE);  // fix the size to a constant after the allocation
+```
+[See https://github.com/diffblue/cbmc/issues/7012 to read more about the workaround and track the fix]
+
+## Performance impact of using CBMC's array theory feature.
+
+CBMC’s array theory generates a number of constraints that is quadratic in the number of accesses to an array, and could be slower in cases with large number of accesses (worse for write accesses). However, unlike the bit-vector encoding, the number of constraints is not dependent on the size of the array itself.
+
+Hence, array theory is better when you have a small number of accesses with non-constant index into a very large array. An example of this is when you want to reason about a single insertion of an element at a non-constant index in a large array.
+