From 59210587bf7e73ee5bd940a5c2817b54be08e3bf Mon Sep 17 00:00:00 2001 From: Boyan-MILANOV Date: Fri, 26 Aug 2022 11:05:35 +0200 Subject: [PATCH 1/5] Support exporting constraints to smtlibv2 --- bindings/python/py_maat.cpp | 1 + bindings/python/py_solver.cpp | 15 +++++++++++++++ bindings/python/python_bindings.hpp | 7 ++++++- bindings/python/util.cpp | 17 +++++++++++++++++ src/include/maat/solver.hpp | 20 ++++++++++++++++++++ 5 files changed, 59 insertions(+), 1 deletion(-) diff --git a/bindings/python/py_maat.cpp b/bindings/python/py_maat.cpp index 47aa9f64..e97f876a 100644 --- a/bindings/python/py_maat.cpp +++ b/bindings/python/py_maat.cpp @@ -25,6 +25,7 @@ PyMethodDef module_methods[] = { {"MaatEngine", (PyCFunction)maat_MaatEngine, METH_VARARGS, "Create a new DSE engine"}, // Solver {"Solver", (PyCFunction)maat_Solver, METH_NOARGS, "Create a constraint solver"}, + {"constraints_to_smt2", (PyCFunction)maat_constraints_to_smt2, METH_VARARGS, "Convert a list of constraints to an SMTlibv2 string"}, // SimpleStateManager {"SimpleStateManager", (PyCFunction)maat_SimpleStateManager, METH_VARARGS, "Create a new helper for serializing/deserializing engine states"}, // EVM diff --git a/bindings/python/py_solver.cpp b/bindings/python/py_solver.cpp index ece55b0d..954a5d42 100644 --- a/bindings/python/py_solver.cpp +++ b/bindings/python/py_solver.cpp @@ -164,6 +164,21 @@ PyObject* maat_Solver(PyObject* module) return PySolver_FromSolver(res); } +PyObject* maat_constraints_to_smt2(PyObject* self, PyObject* args) +{ + PyObject* py_constraints; + std::vector constraints; + if (not PyArg_ParseTuple(args, "O", &py_constraints)) + return NULL; + + PyObject* fail = py_to_native(py_constraints, constraints); + if (fail != nullptr) + return fail; + + std::string res = solver::constraints_to_smt2(constraints); + return PyUnicode_FromString(res.c_str()); +} + } // namespace py } // namespace maat diff --git a/bindings/python/python_bindings.hpp b/bindings/python/python_bindings.hpp index 375dfbed..7246b5df 100644 --- a/bindings/python/python_bindings.hpp +++ b/bindings/python/python_bindings.hpp @@ -258,6 +258,7 @@ typedef struct{ } Solver_Object; PyObject* get_Solver_Type(); PyObject* maat_Solver(PyObject* module); +PyObject* maat_constraints_to_smt2(PyObject* module, PyObject* args); #define as_solver_object(x) (*((Solver_Object*)x)) #endif @@ -355,7 +356,7 @@ PyObject* get_EVMTransactionResult_Type(); PyObject* PyEVMTxResult_FromTxResult(env::EVM::TransactionResult*); #define as_tx_result_object(x) (*((EVMTransactionResult_Object*)x)) -// Return the contract associated with an engine +// EVM helper functions PyObject* maat_contract(PyObject* mod, PyObject* args); PyObject* maat_new_evm_runtime(PyObject* mod, PyObject* args); PyObject* maat_increment_block_timestamp(PyObject* mod, PyObject* args); @@ -369,6 +370,10 @@ PyObject* maat_allow_symbolic_keccak(PyObject* mod, PyObject* args); PyObject* native_to_py(const std::vector&); PyObject* native_to_py(const std::unordered_set& constraints); +// Transform a list of python objects into native objects. Returns a +// python error on error, and NULL on success +PyObject* py_to_native(PyObject* list, std::vector& dest); + // Python bigint into multiprecision number // num MUST be a PyLong object (no further type checks in the function) Number bigint_to_number(size_t bits, PyObject* num); diff --git a/bindings/python/util.cpp b/bindings/python/util.cpp index a865faee..52106b3e 100644 --- a/bindings/python/util.cpp +++ b/bindings/python/util.cpp @@ -48,6 +48,23 @@ PyObject* native_to_py(const std::unordered_set& constraints) return list; } +PyObject* py_to_native(PyObject* list, std::vector& dest) +{ + if (!PyList_Check(list) ) + return PyErr_Format(PyExc_TypeError, "Expected list of constraints"); + + for (int i = 0; i < PyList_Size(list); i++) + { + PyObject* val = PyList_GetItem(list, i); + if (!PyObject_TypeCheck(val, (PyTypeObject*)get_Constraint_Type())) + { + return PyErr_Format(PyExc_TypeError, "List contains object which is not a 'Constraint'"); + } + dest.push_back(*as_constraint_object(val).constr); + } + return nullptr; // return null on success +} + Number bigint_to_number(size_t bits, PyObject* num) { if (bits <= 64) diff --git a/src/include/maat/solver.hpp b/src/include/maat/solver.hpp index 87906f4b..1ba92abf 100644 --- a/src/include/maat/solver.hpp +++ b/src/include/maat/solver.hpp @@ -78,8 +78,28 @@ class SolverZ3 : public Solver virtual std::shared_ptr get_model(); virtual VarContext* _get_model_raw(); }; + +// Forward decl +z3::expr constraint_to_z3(z3::context* c, const Constraint& constr); + +/// Convert a set of constraints into SMTlibv2 format +template< template< typename ELEM, typename ALLOC = std::allocator> class C> +std::string constraints_to_smt2(const C& constraints) { + auto ctx = new z3::context(); + auto sol = new z3::solver(*ctx); + for (auto c : constraints) + sol->add(constraint_to_z3(ctx, c)); + std::string res = sol->to_smt2(); + delete sol; + delete ctx; + return res; +} + #endif + + + /** \} */ // doxygen groupe Solver } // namespace solver } // namespace maat From 5111d37da723a498f7dcf767fd9cd170f57d1bbf Mon Sep 17 00:00:00 2001 From: Boyan-MILANOV Date: Fri, 26 Aug 2022 13:34:32 +0200 Subject: [PATCH 2/5] Add boolector support in cmake --- CMakeLists.txt | 6 ++++++ bindings/bindings.cmake | 6 ++++++ cmake/install-config.cmake.in | 5 +++++ cmake/variables.cmake | 1 + 4 files changed, 18 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index c7be0169..a88c7caf 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -130,6 +130,12 @@ if(maat_USE_Z3) target_compile_definitions(maat_maat PUBLIC MAAT_Z3_BACKEND=1 MAAT_HAS_SOLVER_BACKEND=1) endif() +if(maat_USE_BOOLECTOR) + find_package(Boolector) + target_link_libraries(maat_maat PUBLIC Boolector::boolector) + target_compile_definitions(maat_maat PUBLIC MAAT_BOOLECTOR_BACKEND=1) +endif() + if(maat_USE_LIEF) find_package(LIEF 0.12 REQUIRED) target_link_libraries(maat_maat PUBLIC LIEF::LIEF) diff --git a/bindings/bindings.cmake b/bindings/bindings.cmake index 522cf87c..0fa7f66f 100644 --- a/bindings/bindings.cmake +++ b/bindings/bindings.cmake @@ -81,6 +81,12 @@ if(maat_USE_Z3) target_compile_definitions(maat_python PRIVATE MAAT_Z3_BACKEND=1 MAAT_HAS_SOLVER_BACKEND=1) endif() +if(maat_USE_BOOLECTOR) + find_package(Boolector) + target_link_libraries(maat_python PRIVATE Boolector::boolector) + target_compile_definitions(maat_python PUBLIC MAAT_BOOLECTOR_BACKEND=1) +endif() + if(maat_USE_LIEF) target_link_libraries(maat_python PRIVATE LIEF::LIEF) target_compile_definitions(maat_python PRIVATE MAAT_LIEF_BACKEND=1 MAAT_HAS_LOADER_BACKEND=1) diff --git a/cmake/install-config.cmake.in b/cmake/install-config.cmake.in index 8bd52a56..4d9a0987 100644 --- a/cmake/install-config.cmake.in +++ b/cmake/install-config.cmake.in @@ -16,6 +16,11 @@ if("${maat_USE_Z3}") find_dependency(Z3) endif() +set(maat_USE_BOOLECTOR @maat_USE_BOOLECTOR@) +if("${maat_USE_BOOLECTOR}") + find_dependency(Boolector) +endif() + set(maat_USE_LIEF @maat_USE_LIEF@) if("${maat_USE_LIEF}") find_dependency(LIEF) diff --git a/cmake/variables.cmake b/cmake/variables.cmake index 87433255..d31dd1a0 100644 --- a/cmake/variables.cmake +++ b/cmake/variables.cmake @@ -18,6 +18,7 @@ endif() # technically require but are almost always desirable to find. We include # these options to let an advanced user implement their own backends option(maat_USE_Z3 "Build with Z3 solver backend" ON) +option(maat_USE_BOOLECTOR "Build with Boolector solver backend" OFF) option(maat_USE_LIEF "Build with LIEF loader backend" ON) # Optionally use vendored dependencies From 327d6da9ea54edd5a117ec3d6df7e075591b22fe Mon Sep 17 00:00:00 2001 From: Boyan-MILANOV Date: Fri, 26 Aug 2022 14:14:43 +0200 Subject: [PATCH 3/5] Add class for boolector solver --- CMakeLists.txt | 1 + src/include/maat/solver.hpp | 22 +++++++++--- src/solver/solver_btor.cpp | 68 +++++++++++++++++++++++++++++++++++++ 3 files changed, 87 insertions(+), 4 deletions(-) create mode 100644 src/solver/solver_btor.cpp diff --git a/CMakeLists.txt b/CMakeLists.txt index a88c7caf..c030d30f 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -61,6 +61,7 @@ add_library(maat_maat src/serialization/serialization_helpers.cpp src/serialization/serializer.cpp src/solver/solver.cpp + src/solver/solver_btor.cpp src/solver/solver_z3.cpp src/third-party/murmur3/murmur3.c src/third-party/keccak/sha3.cpp diff --git a/src/include/maat/solver.hpp b/src/include/maat/solver.hpp index 1ba92abf..80067f2c 100644 --- a/src/include/maat/solver.hpp +++ b/src/include/maat/solver.hpp @@ -14,7 +14,7 @@ namespace maat namespace solver { - + /** \defgroup solver Solver * \brief The Maat's constraint solver interface */ @@ -94,11 +94,25 @@ std::string constraints_to_smt2(const C& constraints) { delete ctx; return res; } - #endif - - +#ifdef MAAT_BOOLECTOR_BACKEND +class SolverBtor : public Solver +{ +private: + std::list constraints; + bool has_model; ///< Set to true if check() returned true +public: + SolverBtor(); + virtual ~SolverBtor(); + void reset(); + void add(const Constraint& constr); + void pop(); + bool check(); + virtual std::shared_ptr get_model(); + virtual VarContext* _get_model_raw(); +}; +#endif /** \} */ // doxygen groupe Solver } // namespace solver diff --git a/src/solver/solver_btor.cpp b/src/solver/solver_btor.cpp new file mode 100644 index 00000000..61162876 --- /dev/null +++ b/src/solver/solver_btor.cpp @@ -0,0 +1,68 @@ +#ifdef MAAT_BOOLECTOR_BACKEND + +#include "maat/solver.hpp" +#include "maat/stats.hpp" +#include "maat/exception.hpp" + +namespace maat +{ +namespace solver +{ + +SolverBtor::SolverBtor(): Solver(), has_model(false) +{} + +SolverBtor::~SolverBtor() +{} + +void SolverBtor::reset() +{ + constraints.clear(); + has_model = false; + _did_time_out = false; +} + +void SolverBtor::add(const Constraint& constr) +{ + constraints.push_back(constr); + has_model = false; +} + +void SolverBtor::pop() +{ + constraints.pop_back(); +} + +bool SolverBtor::check() +{ + // If already has model, don't recompute it + if (has_model) + return true; + + // Statistics + MaatStats::instance().start_solving(); + + // TODO + + // Statistics + MaatStats::instance().done_solving(); + + return has_model; +} + +std::shared_ptr SolverBtor::get_model() +{ + return std::shared_ptr(_get_model_raw()); +} + +VarContext* SolverBtor::_get_model_raw() +{ + if (not has_model) + return nullptr; + + // TODO +} + +} // namespace solver +} // namespace maat +#endif // #ifdef MAAT_BOOLECTOR_BACKEND From 1edf64017662347e4f56fbcb0f3c5e4b286369aa Mon Sep 17 00:00:00 2001 From: Boyan-MILANOV Date: Tue, 6 Sep 2022 13:53:13 +0200 Subject: [PATCH 4/5] WIP boolector support --- src/include/maat/solver.hpp | 6 +++++ src/solver/solver.cpp | 3 ++- src/solver/solver_btor.cpp | 47 ++++++++++++++++++++++++++++++++++--- 3 files changed, 52 insertions(+), 4 deletions(-) diff --git a/src/include/maat/solver.hpp b/src/include/maat/solver.hpp index 80067f2c..b5ef3637 100644 --- a/src/include/maat/solver.hpp +++ b/src/include/maat/solver.hpp @@ -9,6 +9,10 @@ #include "z3++.h" #endif +#ifdef MAAT_BOOLECTOR_BACKEND +#include "boolector/boolector.h" +#endif + namespace maat { @@ -99,6 +103,8 @@ std::string constraints_to_smt2(const C& constraints) { #ifdef MAAT_BOOLECTOR_BACKEND class SolverBtor : public Solver { +private: + Btor* btor; private: std::list constraints; bool has_model; ///< Set to true if check() returned true diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index ccc6db95..79cd4dfa 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -25,7 +25,8 @@ bool Solver::did_time_out() const std::unique_ptr new_solver() { #ifdef MAAT_Z3_BACKEND - return std::make_unique(); + // DEBUG return std::make_unique(); + return std::make_unique(); #else return nullptr; #endif diff --git a/src/solver/solver_btor.cpp b/src/solver/solver_btor.cpp index 61162876..2d72b4a7 100644 --- a/src/solver/solver_btor.cpp +++ b/src/solver/solver_btor.cpp @@ -3,6 +3,7 @@ #include "maat/solver.hpp" #include "maat/stats.hpp" #include "maat/exception.hpp" +#include namespace maat { @@ -10,16 +11,24 @@ namespace solver { SolverBtor::SolverBtor(): Solver(), has_model(false) -{} +{ + btor = boolector_new(); + boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1); + boolector_set_opt (btor, BTOR_OPT_INCREMENTAL, 1); +} SolverBtor::~SolverBtor() -{} +{ + boolector_delete(btor); + btor = nullptr; +} void SolverBtor::reset() { constraints.clear(); has_model = false; _did_time_out = false; + boolector_reset_assumptions(btor); } void SolverBtor::add(const Constraint& constr) @@ -42,7 +51,39 @@ bool SolverBtor::check() // Statistics MaatStats::instance().start_solving(); - // TODO + boolector_reset_assumptions(btor); + + // Dump constraints to temporary file + // TODO(boyan): use mkstemp instead of tmpnam + const char *smt_file = tmpnam(NULL); // Get temp name + if (smt_file == nullptr) + throw solver_exception("SolverBtor::check(): couldn't create temporary filename"); + std::ofstream f(smt_file); + if (not f.good()) + throw solver_exception("SolverBtor::check(): couldn't create temporary SMT file"); + std::string smt_string = constraints_to_smt2(constraints); + f << smt_string; + f.close(); + + // Load SMT in boolector + int status = boolector_parse_smt2( + btor, + nullptr, // infile + smt_file, // infile_name + nullptr, // outfile + nullptr, // error_msg + nullptr // status + ); + if (status != BOOLECTOR_PARSE_UNKNOWN) + throw solver_exception( + Fmt() << "SolverBtor::check(): error parsing SMT file: " + << smt_file >> Fmt::to_str + ); + status = boolector_sat(btor); + has_model = (status == BOOLECTOR_SAT); + + // Remove temporary file + remove(smt_file); // Statistics MaatStats::instance().done_solving(); From e6ec97980fad8a2686b5f2db5b02fa056c0a630d Mon Sep 17 00:00:00 2001 From: Boyan-MILANOV Date: Mon, 12 Sep 2022 11:44:47 +0200 Subject: [PATCH 5/5] WIP boolector support --- src/include/maat/solver.hpp | 9 +++- src/include/maat/varcontext.hpp | 1 + src/solver/solver_btor.cpp | 95 +++++++++++++++++++++++++++------ src/solver/solver_z3.cpp | 41 +++++++++++--- 4 files changed, 122 insertions(+), 24 deletions(-) diff --git a/src/include/maat/solver.hpp b/src/include/maat/solver.hpp index b5ef3637..a4fc9470 100644 --- a/src/include/maat/solver.hpp +++ b/src/include/maat/solver.hpp @@ -93,11 +93,14 @@ std::string constraints_to_smt2(const C& constraints) { auto sol = new z3::solver(*ctx); for (auto c : constraints) sol->add(constraint_to_z3(ctx, c)); - std::string res = sol->to_smt2(); + std::string res = sol->to_smt2(); delete sol; delete ctx; return res; } + +/// Create a VarContext from an smtlib2 model +VarContext* ctx_from_smt2(const char* string); #endif #ifdef MAAT_BOOLECTOR_BACKEND @@ -105,6 +108,8 @@ class SolverBtor : public Solver { private: Btor* btor; + // Set to file that holds the current computed model, or to NULL + const char * model_file; private: std::list constraints; bool has_model; ///< Set to true if check() returned true @@ -117,6 +122,8 @@ class SolverBtor : public Solver bool check(); virtual std::shared_ptr get_model(); virtual VarContext* _get_model_raw(); +private: + void reset_btor(); }; #endif diff --git a/src/include/maat/varcontext.hpp b/src/include/maat/varcontext.hpp index 8dc37ac2..47eecb42 100644 --- a/src/include/maat/varcontext.hpp +++ b/src/include/maat/varcontext.hpp @@ -92,6 +92,7 @@ class VarContext: public serial::Serializable void print(std::ostream& os) const; ///< Print the context to a stream Endian endianness() const; ///< Return endianness std::set contained_vars() const; ///< Return the contained symbolic variables + public: virtual serial::uid_t class_uid() const; virtual void dump(serial::Serializer& s) const; diff --git a/src/solver/solver_btor.cpp b/src/solver/solver_btor.cpp index 2d72b4a7..1d160ab4 100644 --- a/src/solver/solver_btor.cpp +++ b/src/solver/solver_btor.cpp @@ -10,11 +10,13 @@ namespace maat namespace solver { -SolverBtor::SolverBtor(): Solver(), has_model(false) +SolverBtor::SolverBtor(): + Solver(), + has_model(false), + btor(nullptr), + model_file(nullptr) { - btor = boolector_new(); - boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1); - boolector_set_opt (btor, BTOR_OPT_INCREMENTAL, 1); + reset_btor(); } SolverBtor::~SolverBtor() @@ -23,12 +25,27 @@ SolverBtor::~SolverBtor() btor = nullptr; } +void SolverBtor::reset_btor() +{ + if (btor != nullptr) + { + // TODO(boyan) + // DEBUG: are these calls useful ? + boolector_reset_assumptions(btor); + boolector_release_all(btor); + boolector_delete(btor); + } + btor = boolector_new(); + boolector_set_opt (btor, BTOR_OPT_MODEL_GEN, 1); + boolector_set_opt (btor, BTOR_OPT_INCREMENTAL, 1); +} + void SolverBtor::reset() { constraints.clear(); has_model = false; _did_time_out = false; - boolector_reset_assumptions(btor); + reset_btor(); } void SolverBtor::add(const Constraint& constr) @@ -48,11 +65,11 @@ bool SolverBtor::check() if (has_model) return true; + reset_btor(); + // Statistics MaatStats::instance().start_solving(); - boolector_reset_assumptions(btor); - // Dump constraints to temporary file // TODO(boyan): use mkstemp instead of tmpnam const char *smt_file = tmpnam(NULL); // Get temp name @@ -65,25 +82,40 @@ bool SolverBtor::check() f << smt_string; f.close(); + std::cout << "DEBUG SMT QUERY iN " << smt_file << "\n"; + // Load SMT in boolector + // TODO(boyan): don't reopen smt_file + // TODO(boyan): don't hardcode dev/null but make it dependent on + // the platform, and find a solution for Windows + FILE* infile = fopen(smt_file, "r"); + FILE* outfile = fopen("/dev/null", "w"); + char* error_msg; + int _status; int status = boolector_parse_smt2( btor, - nullptr, // infile + infile, // infile smt_file, // infile_name - nullptr, // outfile - nullptr, // error_msg - nullptr // status + outfile, // outfile + &error_msg, // error_msg + &_status // status ); - if (status != BOOLECTOR_PARSE_UNKNOWN) + fclose(outfile); + fclose(infile); + + // DEBUG + // if (status == BOOLECTOR_PARSE_UNKNOWN) + // status = boolector_sat(btor); + if (status == BOOLECTOR_PARSE_UNKNOWN) throw solver_exception( - Fmt() << "SolverBtor::check(): error parsing SMT file: " + Fmt() << "SolverBtor::check(): error solving SMT file: " << smt_file >> Fmt::to_str ); - status = boolector_sat(btor); + has_model = (status == BOOLECTOR_SAT); // Remove temporary file - remove(smt_file); + // DEBUG remove(smt_file); // Statistics MaatStats::instance().done_solving(); @@ -101,7 +133,38 @@ VarContext* SolverBtor::_get_model_raw() if (not has_model) return nullptr; - // TODO + // TODO(boyan): don't hardcode + if (model_file == nullptr) + { + model_file = tmpnam(NULL); // Get temp name + if (model_file == nullptr) + throw solver_exception("SolverBtor::_get_model_raw(): couldn't create temporary filename"); + } + FILE* f = fopen(model_file, "w"); + boolector_print_model(btor, "smt2", f); + fclose(f); + + std::ifstream in(model_file, std::ios::binary); + std::vector data( + (std::istreambuf_iterator(in)), + (std::istreambuf_iterator()) + ); + std::vector clean_data{'(', 'm', 'o', 'd', 'e', 'l', '\n'}; + for (int i = 2; i < data.size(); i++) + { + // DEBUG remove false?? + if ( + false && i+2 < data.size() && data[i] == '\n' + && data[i+1] == ' ' && data[i+2] == ' ' + ){ + clean_data.push_back('\n'); + i += 2; + } + else + clean_data.push_back(data[i]); + } + remove(model_file); + ctx_from_smt2(clean_data.data()); } } // namespace solver diff --git a/src/solver/solver_z3.cpp b/src/solver/solver_z3.cpp index c42af90d..c052998e 100644 --- a/src/solver/solver_z3.cpp +++ b/src/solver/solver_z3.cpp @@ -205,16 +205,12 @@ std::shared_ptr SolverZ3::get_model() return std::shared_ptr(_get_model_raw()); } -VarContext* SolverZ3::_get_model_raw() +VarContext* z3_model_to_varcontext(z3::model& m, z3::context& ctx) { - if (not has_model) - return nullptr; - - z3::model m = sol->get_model(); - auto res = new VarContext(_model_id_cnt++); + auto res = new VarContext(); for (int i = 0; i < m.num_consts(); i++) { - size_t size = Z3_get_bv_sort_size(*ctx, m.get_const_interp(m[i]).get_sort()); + size_t size = Z3_get_bv_sort_size(ctx, m.get_const_interp(m[i]).get_sort()); Number val(size); if (size <= 64) val.set_cst(m.get_const_interp(m[i]).get_numeral_uint64()); @@ -229,6 +225,37 @@ VarContext* SolverZ3::_get_model_raw() return res; } +VarContext* SolverZ3::_get_model_raw() +{ + if (not has_model) + return nullptr; + + z3::model m = sol->get_model(); + return z3_model_to_varcontext(m, *ctx); +} + +VarContext* ctx_from_smt2(const char* string) +{ + auto ctx = new z3::context(); + auto sol = new z3::solver(*ctx); + std::cout << "DEBUG smt2 string: \n" << string << "\n"; + sol->from_string(string); + switch (sol->check()) + { + case z3::check_result::sat: + break; + default: + throw solver_exception("ctx_from_smt2: z3 failed to compute model"); + } + z3::model m = sol->get_model(); + std::cout << "DEBUG z3 model " << m << "\n"; + VarContext* res = z3_model_to_varcontext(m, *ctx); + std::cout << "DEBUG ctx " << *res << "\n"; + delete sol; + delete ctx; + return res; +} + } // namespace solver } // namespace maat #endif // #ifdef MAAT_Z3_BACKEND