Merge branch 'master' into lfscTestslfscTests

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;
+}
+