File tree Expand file tree Collapse file tree 2 files changed +8
-4
lines changed
src/org/sosy_lab/java_smt/basicimpl Expand file tree Collapse file tree 2 files changed +8
-4
lines changed Original file line number Diff line number Diff line change @@ -281,7 +281,7 @@ private String sanitize(String formulaStr) {
281
281
// Keep only declaration, definitions and assertion
282
282
builder .append (token ).append ('\n' );
283
283
284
- } else if (Tokenizer .isUnsupportedToken (token )) {
284
+ } else if (Tokenizer .isForbiddenToken (token )) {
285
285
// Throw an exception if the script contains commands like (pop) or (reset) that change the
286
286
// state of the assertion stack.
287
287
// We could keep track of the state of the stack and only consider the formulas that remain
Original file line number Diff line number Diff line change @@ -219,9 +219,9 @@ public static boolean isExitToken(String token) {
219
219
}
220
220
221
221
/**
222
- * Check if this is an unsupported token.
222
+ * Check if this is a forbidden token.
223
223
*
224
- * <p>The list of unsupported tokens contains:
224
+ * <p>The list of forbidden tokens contains:
225
225
*
226
226
* <ul>
227
227
* <li>push
@@ -230,9 +230,13 @@ public static boolean isExitToken(String token) {
230
230
* <li>reset
231
231
* </ul>
232
232
*
233
+ * <p>Forbidden tokens manipulate the stack and are not supported while parsing SMT-lIB2 string.
234
+ * When a forbidden token is found parsing should be aborted by throwing an {@link
235
+ * IllegalArgumentException} exception.
236
+ *
233
237
* <p>Use {@link #tokenize(String)} to turn an SMT-LIB2 script into a string of input tokens.
234
238
*/
235
- public static boolean isUnsupportedToken (String token ) {
239
+ public static boolean isForbiddenToken (String token ) {
236
240
return isPushToken (token )
237
241
| isPopToken (token )
238
242
| isResetAssertionsToken (token )
You can’t perform that action at this time.
0 commit comments