diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-18 10:31:53 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-06-18 17:31:53 +0000 |
commit | 5b15ba18c32ed78190b7e71b6bfb64f1f8b8dcab (patch) | |
tree | 2c27fbe335ba1fd42c452511c1955b2339b53974 /test/api | |
parent | 828702825ab82175029e087eb8911575acd43a82 (diff) |
Make CnfStream::toCNF iterative (#6757)
This commit makes toCNF() iterative to avoid this issue.
Note that the order in which nodes are visited and thus SatLiterals are
created remains the same.
Fixes #6111
Diffstat (limited to 'test/api')
-rw-r--r-- | test/api/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/api/issue6111.cpp | 58 |
2 files changed, 59 insertions, 0 deletions
diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index e9fd47261..4811cca1b 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -51,6 +51,7 @@ cvc5_add_api_test(smt2_compliance) cvc5_add_api_test(two_solvers) cvc5_add_api_test(issue5074) cvc5_add_api_test(issue4889) +cvc5_add_api_test(issue6111) # if we've built using libedit, then we want the interactive shell tests if (USE_EDITLINE) diff --git a/test/api/issue6111.cpp b/test/api/issue6111.cpp new file mode 100644 index 000000000..bd7be2ad0 --- /dev/null +++ b/test/api/issue6111.cpp @@ -0,0 +1,58 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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 issue #6111 + * + */ +#include <iostream> +#include <vector> + +#include "api/cpp/cvc5.h" + +using namespace cvc5::api; +using namespace std; + +int main() +{ + Solver solver; + solver.setLogic("QF_BV"); + Sort bvsort12979 = solver.mkBitVectorSort(12979); + Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1"); + Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10); + + vector<Term> args1; + args1.push_back(zero); + args1.push_back(input2_1); + Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1); + solver.assertFormula(bvult_res); + + Sort bvsort4 = solver.mkBitVectorSort(4); + Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42"); + Sort bvsort8 = solver.mkBitVectorSort(8); + Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43"); + + vector<Term> args2; + args2.push_back(concat_result_42); + args2.push_back( + solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43})); + solver.assertFormula(solver.mkTerm(EQUAL, args2)); + + vector<Term> args3; + args3.push_back(concat_result_42); + args3.push_back( + solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43})); + solver.assertFormula(solver.mkTerm(EQUAL, args3)); + + cout << solver.checkSat() << endl; + + return 0; +} |