Array theory: implement weakly equivalent arrays

This implements Christ and Hoenicke's Weakly Equivalent Arrays
(https://arxiv.org/pdf/1405.6939.pdf) with in-place depth-first path
enumeration.

Co-authored-by: Michael Tautschnig <[email protected]>

Author: kroening

regression/cbmc/Array_UF22/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 main.c
 --arrays-uf-always --no-propagation
 ^VERIFICATION SUCCESSFUL$