First incremental smt backed doc draft

Author: Enrico Steffinlongo

doc/cprover-manual/index.md

@@ -31,4 +31,8 @@
 [Integration into Build Systems with goto-cc](goto-cc/),
 [Integration with Visual Studio builds](visual-studio/)
 
-## 10. [The CPROVER API Reference](api/)
+## 10. New SMT backend
+
+[New SMT2 incremental backend](smt2-incr/)
+
+## 11. [The CPROVER API Reference](api/)

doc/cprover-manual/smt2-incr.md

@@ -0,0 +1,40 @@
+[CPROVER Manual TOC](../)
+
+## Incremental SMT backend
+
+CBMC comes with a solver-agnostic incremental SMT backend.
+
+The SMT incremental backend supports the following `C` primitives:
+
+- Bit vector arithmetics
+- Pointers
+- Arrays (support is currently incomplete)
+
+Primitive not supported are:
+
+- Floating point values and arithmetics
+- Structs
+
+Requirement to use the incremental SMT backend is to have a solver which accepts
+SMTlib 2.6 incremental input from the standard input and that supports the
+`QF_AUFBV` (Quantifier Free Array Uninterpreted Functions and Bit Vectors).
+
+To use this functionality it is enough to add the argument
+`--incremental-smt2-solver <cmd>` where `<cmd>` is the command to invoke the SMT
+solver of choice using the interactive mode and accepting input from the
+standard input.
+
+Examples are:
+
+1. `--incremental-smt2-solver 'z3 -smt2 -in'` to use the Z3 solver.
+2. `--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental'` to use the
+   CVC5 solver.
+
+Note that the solver has to be user-supplied and CBMC does not come packaged
+with any SMT solver, so the solver name must be in the `PATH` or an executable
+with full path must be provided.
+
+Also note that because of the partial array support, the `--slice-formula`
+argument must be passed to CBMC, so that unsupported part of the automatically
+added preamble will be removed.
+