Skip to content

Commit 4b9f33f

Browse files
Bitwuzla: Fix handling of quoted symbol names while parsing SMTLIB formulas
1 parent 72eac3b commit 4b9f33f

File tree

1 file changed

+7
-3
lines changed

1 file changed

+7
-3
lines changed

src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -137,12 +137,16 @@ public Term parseImpl(String formulaStr) throws IllegalArgumentException {
137137
// Process the symbols from the parser
138138
Map_TermTerm subst = new Map_TermTerm();
139139
for (Term term : declared) {
140-
if (cache.containsRow(term.symbol())) {
140+
String symbol = term.symbol();
141+
if (symbol.startsWith("|") && symbol.endsWith("|")) {
142+
symbol = symbol.substring(1, symbol.length() - 1);
143+
}
144+
if (cache.containsRow(symbol)) {
141145
// Symbol is from the context: add the original term to the substitution map
142-
subst.put(term, cache.get(term.symbol(), term.sort()));
146+
subst.put(term, cache.get(symbol, term.sort()));
143147
} else {
144148
// Symbol is new, add it to the context
145-
cache.put(term.symbol(), term.sort(), term);
149+
cache.put(symbol, term.sort(), term);
146150
}
147151
}
148152

0 commit comments

Comments
 (0)