Skip to content

Commit 6a448ef

Browse files
committed
fix compilation: change exception type to plain Error instead of SolverException.
This change avoids an API change (that was already reverted before). CVC4 runs (or is) out of support and the related issue with Unicode strings will not be fixed.
1 parent cc809d2 commit 6a448ef

File tree

1 file changed

+3
-4
lines changed

1 file changed

+3
-4
lines changed

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

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -124,8 +124,7 @@ protected void popImpl() {
124124
}
125125

126126
@Override
127-
protected @Nullable Void addConstraintImpl(BooleanFormula pF)
128-
throws InterruptedException, SolverException {
127+
protected @Nullable Void addConstraintImpl(BooleanFormula pF) throws InterruptedException {
129128
Preconditions.checkState(!closed);
130129
setChanged();
131130
if (incremental) {
@@ -134,11 +133,11 @@ protected void popImpl() {
134133
return null;
135134
}
136135

137-
private void assertFormula(BooleanFormula pF) throws SolverException {
136+
private void assertFormula(BooleanFormula pF) {
138137
try {
139138
smtEngine.assertFormula(importExpr(creator.extractInfo(pF)));
140139
} catch (Exception cvc4Exception) {
141-
throw new SolverException(
140+
throw new AssertionError(
142141
String.format("CVC4 crashed while adding the constraint '%s'", pF), cvc4Exception);
143142
}
144143
}

0 commit comments

Comments
 (0)