Skip to content

Commit

Permalink
(C++) Added test cases for sosy-lab/java-smt#310
Browse files Browse the repository at this point in the history
  • Loading branch information
daniel-raffler committed Jan 2, 2024
1 parent de8dc61 commit 34d7bbb
Show file tree
Hide file tree
Showing 4 changed files with 112 additions and 0 deletions.
3 changes: 3 additions & 0 deletions test/api/cpp/CMakeLists.txt
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
38 changes: 38 additions & 0 deletions test/api/cpp/javasmt-parallel1.cpp
Original file line number Diff line number Diff line change
@@ -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 <cvc5/cvc5.h>
#include <thread>

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();
}
37 changes: 37 additions & 0 deletions test/api/cpp/javasmt-parallel2.cpp
Original file line number Diff line number Diff line change
@@ -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 <cvc5/cvc5.h>
#include <thread>

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();
}
34 changes: 34 additions & 0 deletions test/api/cpp/javasmt-parallel3.cpp
Original file line number Diff line number Diff line change
@@ -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 <cvc5/cvc5.h>
#include <thread>

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();
}

0 comments on commit 34d7bbb

Please sign in to comment.