Fix test failures due to Z3 v4.12 (#167)

* gitignore: Ignore 'maat_state_*' files from tests

* Fix test failures due to Z3 4.12

Upgrading Z3 causes test failures due to incomplete model for all
expected variables. Previous versions reported values for all variables,
but now tests should check whether a value has been assigned before
testing the value.

* Don't fail fast matrix

.github/workflows/ci.yml

@@ -99,6 +99,7 @@ jobs:
 
   test:
     strategy:
+      fail-fast: false
       matrix:
         os: [
           # TODO: windows,

.gitignore

@@ -7,3 +7,4 @@ cmake-build-*/
 prefix/
 CMakeLists.txt.user
 CMakeUserPresets.json
+maat_state_*

tests/adv-tests/test_evm.cpp

@@ -49,8 +49,9 @@ int solve_symbolic_storage()
     sol->add(v == 2);
     nb += _assert(sol->check(), "Couldn't find model to solve symbolic storage read");
     auto model = sol->get_model();
-    nb += _assert(model->get_as_number("b").equal_to(model->get_as_number("d")), "Got wrong model when solving symbolic storage");
-    nb += _assert(not model->get_as_number("c").equal_to(model->get_as_number("d")), "Got wrong model when solving symbolic storage");
+    nb += _assert(not model->contains("a") or not model->get_as_number("a").equal_to(model->get_as_number("d")), "Got wrong model when solving symbolic storage a == d");
+    nb += _assert(model->get_as_number("b").equal_to(model->get_as_number("d")), "Got wrong model when solving symbolic storage b != d");
+    nb += _assert(not model->contains("c") or not model->get_as_number("c").equal_to(model->get_as_number("d")), "Got wrong model when solving symbolic storage c == d");
 
     // Write concrete, read symbolic
     contract.storage->write(Value(256, 0xaaaa), Value(256, 5), s);
@@ -70,8 +71,8 @@ int solve_symbolic_storage()
     nb += _assert(sol->check(), "Couldn't find model to solve symbolic storage read");
     model = sol->get_model();
     nb += _assert(model->get_as_number("a").equal_to(Number(256, 0xdedede)), "Got wrong model when solving symbolic storage");
-    nb += _assert(not model->get_as_number("b").equal_to(Number(256, 0xdedede)), "Got wrong model when solving symbolic storage");
-    nb += _assert(not model->get_as_number("c").equal_to(Number(256, 0xdedede)), "Got wrong model when solving symbolic storage");
+    nb += _assert(not model->contains("b") or not model->get_as_number("b").equal_to(Number(256, 0xdedede)), "Got wrong model when solving symbolic storage");
+    nb += _assert(not model->contains("c") or not model->get_as_number("c").equal_to(Number(256, 0xdedede)), "Got wrong model when solving symbolic storage");
 
     // Overwrite symbolic address
     contract.storage->write(Value(exprvar(256, "a")), Value(256, 15), s);