Changes in this commit were made in collaboration with Stephen
McCamant(smccaman@umn.edu). This commit fixes a bug in formula_manager
where it was not recursively rewriting the index expression used in a
table lookup for the solver. This was leading to a later error in
ocaml/smt_lib2.ml because it would run into a variable granularity
memory access variable which should have been turned into a scalar
variable earlier. Further explanation for this rewriting can be found in
the comments above formula_manager.ml#rewrite_mem_to_scalar.
Changes in this commit were made in collaboration with Stephen McCamant(smccaman@umn.edu). This commit fixes a bug in formula_manager where it was not recursively rewriting the index expression used in a table lookup for the solver. This was leading to a later error in ocaml/smt_lib2.ml because it would run into a variable granularity memory access variable which should have been turned into a scalar variable earlier. Further explanation for this rewriting can be found in the comments above formula_manager.ml#rewrite_mem_to_scalar.