blob: b41258c29eb014df85de091ee982787d0620a7ed (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
|
/********************* */
/*! \file BitVectorsAndArrays.java
** \verbatim
** Top contributors (to current version):
** Andres Noetzli
** This file is part of the CVC4 project.
** Copyright (c) 2009-2020 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.\endverbatim
**
** \brief Test case for issue #2846
**
** This test case tests whether the dependency information for keeping the
** ExprManager alive is maintained correctly.
**/
import edu.stanford.CVC4.*;
import org.junit.Test;
public class Issue2846 {
static {
System.loadLibrary("cvc4jni");
}
@Test
public void test() throws InterruptedException {
testInternal();
gc("h");
}
private static void testInternal() throws InterruptedException {
ExprManager em = new ExprManager();
SmtEngine smt = new SmtEngine(em);
smt.setOption("produce-models", new SExpr(true));
Expr x = em.mkVar("x", em.integerType());
Expr y = em.mkVar("y", em.integerType());
Expr z = em.mkVar("z", em.integerType());
gc("a");
Expr a1 = em.mkExpr(Kind.GT, x, em.mkExpr(Kind.PLUS, y, z));
gc("b");
smt.assertFormula(a1);
gc("c");
Expr a2 = em.mkExpr(Kind.LT, y, z);
gc("d");
smt.assertFormula(a2);
gc("e");
System.out.println(a1);
System.out.println(a2);
gc("f");
Result res = smt.checkSat();
gc("g");
System.out.println("Res = " + res);
System.out.println("x = " + smt.getValue(x));
System.out.println("y = " + smt.getValue(y));
System.out.println("z = " + smt.getValue(z));
}
private static void gc(String msg) throws InterruptedException {
System.out.println("calling gc " + msg);
Thread.sleep(100);
System.gc();
}
}
|
