diff options
Diffstat (limited to 'test/system/two_solvers.cpp')
-rw-r--r-- | test/system/two_solvers.cpp | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test/system/two_solvers.cpp b/test/system/two_solvers.cpp new file mode 100644 index 000000000..c5bea4860 --- /dev/null +++ b/test/system/two_solvers.cpp @@ -0,0 +1,32 @@ +/********************* */ +/*! \file two_smt_engines.cpp + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief A simple test of multiple SmtEngines + ** + ** A simple test of multiple SmtEngines. + **/ + +#include <iostream> +#include <sstream> + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; +using namespace std; + +int main() { + Solver s1; + Solver s2; + Result r = s1.checkEntailed(s1.mkBoolean(true)); + Result r2 = s2.checkEntailed(s2.mkBoolean(true)); + return r.isEntailed() && r2.isEntailed() ? 0 : 1; +} + |