Tests failed under z3 releases after 4.7.1

[Bo-Yuan-Huang]

Describe the bug
Unit tests fail when using z3 of version > 4.7.1

To Reproduce
Steps to reproduce the behavior:

1. Install z3 with version > 4.7.1
2. bjam to build and test the synthesis engine

Expected behavior
Several tests would fail with an assertion failure in z3 (e.g., mismatch types).

Desktop (please complete the following information):

• OS: Ubuntu
• Version: Bionic (18.04 LTS)

Additional context
The breakdown seems to happen in between the following commits:

• pass on merge @ 68043296610733757cba816f3f573339cefc4262
• fail on merge @ 91ef84b8c9734c019afbdcd78788c67340ff084e

[Bo-Yuan-Huang]

capture-output bin/test_mem.test/gcc-4.8/debug/cpp11-on/test_mem
====== BEGIN OUTPUT ======
iram (type mem 8 8)
(readmem iram addr) (type bitvector 8)
(+ (readmem iram addr) 0x1) (type bitvector 8)
(store iram addr (+ (readmem iram addr) 0x1)) (type mem 8 8)

(select iram addr)
(bvadd #x01 (select iram addr))
[default: 0xFF]
[0x80:0x0 0x81:0x1 0x82:0x2 0x83:0x3 0x84:0x4 0x85:0x5 0x86:0x6 0x87:0x7 0x88:0x8 0x89:0x9 0x8A:0xA 0x8B:0xB 0x8C:0xC 0x8D:0xD 0x8E:0xE 0x8F:0xF default: 0xFF]
[0x80:0x0 0x81:0x1 0x82:0x2 0x83:0x3 0x84:0x4 0x85:0x5 0x86:0x6 0x87:0x7 0x88:0x8 0x89:0x9 0x8A:0xA 0x8B:0xB 0x8C:0xC 0x8D:0xD 0x8E:0xE 0x8F:0xF default: 0xFF]
[0x80:0x0 0x81:0x1 0x82:0x2 0x83:0x3 0x84:0x4 0x85:0x5 0x86:0x6 0x87:0x7 0x88:0x8 0x89:0x9 0x8A:0xA 0x8B:0xB 0x8C:0xC 0x8D:0xD 0x8E:0xE 0x8F:0xF default: 0x0]
[(128, 0), (129, 1), (130, 2), (131, 3), (132, 4), (133, 5), (134, 6), (135, 7), (136, 8), (137, 9), (138, 10), (139, 11), (140, 12), (141, 13), (142, 14), (143, 15)]
(define-fun addr () (_ BitVec 8)
#x00)
false
true
python: /usr/include/z3++.h:804: z3::expr::operator Z3_app() const: Assertion `is_app()' failed.
Aborted (core dumped)

EXIT STATUS: 134
====== END OUTPUT ======

LD_LIBRARY_PATH="/home/runner/ILA-Tools/py-tmpl-synth/bin/gcc-4.8/debug/cpp11-on:/usr/bin:/usr/lib:/usr/lib32:/usr/lib64:$LD_LIBRARY_PATH"

export LD_LIBRARY_PATH

PYTHONPATH="bin/gcc-4.8/debug/cpp11-on"

export PYTHONPATH
"python" "test/mem.py" > "bin/test_mem.test/gcc-4.8/debug/cpp11-on/test_mem.output" 2>&1
status=$?
echo >> "bin/test_mem.test/gcc-4.8/debug/cpp11-on/test_mem.output"
echo EXIT STATUS: $status >> "bin/test_mem.test/gcc-4.8/debug/cpp11-on/test_mem.output"
if test $status -eq 0 ; then
cp "bin/test_mem.test/gcc-4.8/debug/cpp11-on/test_mem.output" "bin/test_mem.test/gcc-4.8/debug/cpp11-on/test_mem"
fi
verbose=0
if test $status -ne 0 ; then
verbose=1
fi
if test $verbose -eq 1 ; then
echo ====== BEGIN OUTPUT ======
cat "bin/test_mem.test/gcc-4.8/debug/cpp11-on/test_mem.output"
echo ====== END OUTPUT ======
fi
exit $status

...failed capture-output bin/test_mem.test/gcc-4.8/debug/cpp11-on/test_mem...

[Bo-Yuan-Huang]

In release 4.8.0, the value z3::expr returned from model.eval() of source memory (array) will be represented by lambda function, as documented below:
https://github.com/Z3Prover/z3/blob/947fe2ff9c7451d2f192d3453ed4d1eb347cd0f3/RELEASE_NOTES#L59

This can be disabled by setting the top-level parameter model_compression to FALSE.