diff options
Diffstat (limited to 'test/api/issue6111.cpp')
-rw-r--r-- | test/api/issue6111.cpp | 58 |
1 files changed, 58 insertions, 0 deletions
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; +} |