1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Mathias Preiner |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS |
8 |
|
* in the top-level source directory and their institutional affiliations. |
9 |
|
* All rights reserved. See the file COPYING in the top-level source |
10 |
|
* directory for licensing information. |
11 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Test for issue #6111 |
14 |
|
* |
15 |
|
*/ |
16 |
|
#include <iostream> |
17 |
|
#include <vector> |
18 |
|
|
19 |
|
#include "api/cpp/cvc5.h" |
20 |
|
|
21 |
|
using namespace cvc5::api; |
22 |
|
using namespace std; |
23 |
|
|
24 |
1 |
int main() |
25 |
|
{ |
26 |
2 |
Solver solver; |
27 |
1 |
solver.setLogic("QF_BV"); |
28 |
2 |
Sort bvsort12979 = solver.mkBitVectorSort(12979); |
29 |
2 |
Term input2_1 = solver.mkConst(bvsort12979, "intpu2_1"); |
30 |
2 |
Term zero = solver.mkBitVector(bvsort12979.getBVSize(), "0", 10); |
31 |
|
|
32 |
2 |
vector<Term> args1; |
33 |
1 |
args1.push_back(zero); |
34 |
1 |
args1.push_back(input2_1); |
35 |
2 |
Term bvult_res = solver.mkTerm(BITVECTOR_ULT, args1); |
36 |
1 |
solver.assertFormula(bvult_res); |
37 |
|
|
38 |
2 |
Sort bvsort4 = solver.mkBitVectorSort(4); |
39 |
2 |
Term concat_result_42 = solver.mkConst(bvsort4, "concat_result_42"); |
40 |
2 |
Sort bvsort8 = solver.mkBitVectorSort(8); |
41 |
2 |
Term concat_result_43 = solver.mkConst(bvsort8, "concat_result_43"); |
42 |
|
|
43 |
2 |
vector<Term> args2; |
44 |
1 |
args2.push_back(concat_result_42); |
45 |
1 |
args2.push_back( |
46 |
2 |
solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 7, 4), {concat_result_43})); |
47 |
1 |
solver.assertFormula(solver.mkTerm(EQUAL, args2)); |
48 |
|
|
49 |
2 |
vector<Term> args3; |
50 |
1 |
args3.push_back(concat_result_42); |
51 |
1 |
args3.push_back( |
52 |
2 |
solver.mkTerm(solver.mkOp(BITVECTOR_EXTRACT, 3, 0), {concat_result_43})); |
53 |
1 |
solver.assertFormula(solver.mkTerm(EQUAL, args3)); |
54 |
|
|
55 |
1 |
cout << solver.checkSat() << endl; |
56 |
|
|
57 |
1 |
return 0; |
58 |
3 |
} |