summaryrefslogtreecommitdiff
path: root/src/theory/strings/proof_checker.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/strings/proof_checker.cpp')
-rw-r--r--src/theory/strings/proof_checker.cpp4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/strings/proof_checker.cpp b/src/theory/strings/proof_checker.cpp
index 226db01f6..191e0e16c 100644
--- a/src/theory/strings/proof_checker.cpp
+++ b/src/theory/strings/proof_checker.cpp
@@ -444,11 +444,11 @@ Node StringProofRuleChecker::checkInternal(PfRule id,
SkolemCache sc;
if (id == PfRule::RE_UNFOLD_POS)
{
- conc = RegExpOpr::reduceRegExpPos(atom[0], atom[1], &sc);
+ conc = RegExpOpr::reduceRegExpPos(children[0], &sc);
}
else
{
- conc = RegExpOpr::reduceRegExpNeg(atom[0], atom[1], &sc);
+ conc = RegExpOpr::reduceRegExpNeg(children[0], &sc);
}
return ProofSkolemCache::getWitnessForm(conc);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback