Skip to content

Commit 3ad393c

Browse files
committed
CVC4: add info about broken method.
1 parent 39f9e0a commit 3ad393c

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4SLFormulaManager.java

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,14 @@ protected Expr makeEmptyHeap(Type pT1, Type pT2) {
4545

4646
@Override
4747
protected Expr makeNilElement(Type pType) {
48+
// TODO CVC4 bindings for Java do not support creation of SEP_NIL via mkTerm.
49+
// It is unclear whether this method ever worked.
50+
// CVC4 is deprecated and we will not investigate here.
51+
//
52+
// Executing this method will cause the following exception:
53+
// Illegal argument detected: CVC4::Expr CVC4::ExprManager::mkExpr(CVC4::Kind, CVC4::Expr)
54+
// `kind' is a bad argument; ... Only operator-style expressions are made with mkExpr();
55+
// to make variables and constants, see mkVar(), mkBoundVar(), and mkConst().
4856
return exprManager.mkExpr(Kind.SEP_NIL, pType.mkGroundTerm());
4957
}
5058
}

0 commit comments

Comments
 (0)