1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds |
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 project issue #334 |
14 |
|
* |
15 |
|
*/ |
16 |
|
|
17 |
|
#include "api/cpp/cvc5.h" |
18 |
|
|
19 |
|
using namespace cvc5::api; |
20 |
|
|
21 |
1 |
int main(void) |
22 |
|
{ |
23 |
2 |
Solver slv; |
24 |
1 |
slv.setOption("produce-unsat-cores", "true"); |
25 |
2 |
Sort s1 = slv.mkBitVectorSort(1); |
26 |
2 |
Sort s2 = slv.mkFloatingPointSort(8, 24); |
27 |
2 |
Term val = slv.mkBitVector(32, "10000000110010111010111011000101", 2); |
28 |
2 |
Term t1 = slv.mkFloatingPoint(8, 24, val); |
29 |
2 |
Term t2 = slv.mkConst(s1); |
30 |
2 |
Term t4 = slv.mkTerm(Kind::BITVECTOR_TO_NAT, t2); |
31 |
2 |
Term t5 = slv.mkTerm(Kind::STRING_FROM_CODE, t4); |
32 |
2 |
Term t6 = slv.simplify(t5); |
33 |
2 |
Term t7 = slv.mkTerm(Kind::STRING_LEQ, t5, t6); |
34 |
1 |
slv.assertFormula(t7); |
35 |
1 |
slv.simplify(t1); |
36 |
1 |
} |