diff options
| author | Cristian Cadar <c.cadar@imperial.ac.uk> | 2016-06-23 12:17:02 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2016-06-23 12:17:02 +0100 |
| commit | 83e797ab33aef2749e0f6ffb9b63877085ca4e7c (patch) | |
| tree | 406a8fc982967a7e7e2a883cde75a06671ad6971 /lib/Solver/MetaSMTSolver.cpp | |
| parent | 96ed13583a464538cab900c851bcc7338150772a (diff) | |
| parent | 7bcd56cb0c102d4f662205958b2a5aa6698b86ea (diff) | |
| download | klee-83e797ab33aef2749e0f6ffb9b63877085ca4e7c.tar.gz | |
Merge pull request #409 from hoangmle/fix_metaSMT
Add metaSMT to Travis CI, fix metaSMTBuilder to pass all tests
Diffstat (limited to 'lib/Solver/MetaSMTSolver.cpp')
| -rw-r--r-- | lib/Solver/MetaSMTSolver.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index c4f6a5d0..56964b5d 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -19,11 +19,15 @@ #include <metaSMT/DirectSolver_Context.hpp> #include <metaSMT/backend/Z3_Backend.hpp> #include <metaSMT/backend/Boolector.hpp> -#include <metaSMT/backend/MiniSAT.hpp> -#include <metaSMT/support/run_algorithm.hpp> -#include <metaSMT/API/Stack.hpp> -#include <metaSMT/API/Group.hpp> +#define Expr VCExpr +#define Type VCType +#define STP STP_Backend +#include <metaSMT/backend/STP.hpp> +#undef Expr +#undef Type +#undef STP + #include <errno.h> #include <unistd.h> #include <signal.h> |