diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt index fdb41aa1a10..7108faeb1cd 100644 --- a/test/api/cpp/CMakeLists.txt +++ b/test/api/cpp/CMakeLists.txt @@ -59,6 +59,9 @@ cvc5_add_api_test(issue5074) cvc5_add_api_test(issue4889) cvc5_add_api_test(issue6111) cvc5_add_api_test(javasmt-bug347) +cvc5_add_api_test(javasmt-parallel1) +cvc5_add_api_test(javasmt-parallel2) +cvc5_add_api_test(javasmt-parallel3) cvc5_add_api_test(proj-issue306) cvc5_add_api_test(proj-issue334) cvc5_add_api_test(proj-issue344) diff --git a/test/api/cpp/javasmt-parallel1.cpp b/test/api/cpp/javasmt-parallel1.cpp new file mode 100644 index 00000000000..88f04749ede --- /dev/null +++ b/test/api/cpp/javasmt-parallel1.cpp @@ -0,0 +1,38 @@ + /****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2023 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. + * **************************************************************************** + * + * Test for JavaSMT bug #310 + * https://github.com/sosy-lab/java-smt/issues/310 + */ + +#include +#include + +using namespace cvc5; + +void parallel1(Solver& solver) { + // FIXME: + // Fatal failure within + // void NodeManager::poolRemove(expr::NodeValue*) + // at /home/daniel/workspace/cvc5/build/src/expr/node_manager.h:1083 + // + // Check failure d_nodeValuePool.find(nv) != d_nodeValuePool.end() + // NodeValue is not in the pool! + solver.getBooleanSort(); +}; + +int main() { + Solver solver; + + std::thread task(parallel1, std::ref(solver)); + task.join(); +} diff --git a/test/api/cpp/javasmt-parallel2.cpp b/test/api/cpp/javasmt-parallel2.cpp new file mode 100644 index 00000000000..4b2ba4ab7db --- /dev/null +++ b/test/api/cpp/javasmt-parallel2.cpp @@ -0,0 +1,37 @@ + /****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2023 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. + * **************************************************************************** + * + * Test for JavaSMT bug #310 + * https://github.com/sosy-lab/java-smt/issues/310 + */ + +#include +#include + +using namespace cvc5; + +void parallel2(Term& formula) { + Solver prover; + // FIXME: + // terminate called after throwing an instance of 'cvc5::CVC5ApiException' + // what(): + // Given term is not associated with the node manager of this solver + prover.assertFormula(formula); +}; + +int main() { + Solver solver; + Term formula = solver.mkFalse(); + + std::thread task(parallel2, std::ref(formula)); + task.join(); +} diff --git a/test/api/cpp/javasmt-parallel3.cpp b/test/api/cpp/javasmt-parallel3.cpp new file mode 100644 index 00000000000..bbcf9b2f01f --- /dev/null +++ b/test/api/cpp/javasmt-parallel3.cpp @@ -0,0 +1,34 @@ + /****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Andrew Reynolds, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2023 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. + * **************************************************************************** + * + * Test for JavaSMT bug #310 + * https://github.com/sosy-lab/java-smt/issues/310 + */ + +#include +#include + +using namespace cvc5; + +void parallel3(Solver& solver) { + solver.push(); +}; + +int main() { + Solver solver; + Term varA = solver.mkConst(solver.getBooleanSort(), "a"); + + solver.assertFormula(varA); + + std::thread task(parallel3, std::ref(solver)); + task.join(); +}