summaryrefslogtreecommitdiff
path: root/src/theory/strings/theory_strings.h
diff options
context:
space:
mode:
authorTianyi Liang <tianyi-liang@uiowa.edu>2014-02-12 16:10:07 -0600
committerTianyi Liang <tianyi-liang@uiowa.edu>2014-02-12 16:10:07 -0600
commit2e1d725478eb24433eaf0f70822550966ef53d3d (patch)
tree74902d8444d4441a3674d2b05df19ca7d1b7162a /src/theory/strings/theory_strings.h
parentd5e776a4119ee765b21cfc2f3c31abcd1c07d4e8 (diff)
bug fix for reverse check
Diffstat (limited to 'src/theory/strings/theory_strings.h')
-rw-r--r--src/theory/strings/theory_strings.h1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 5d8ff016f..3143d6e89 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -224,6 +224,7 @@ private:
bool checkSimple();
bool checkNormalForms();
+ void checkDeqNF();
bool checkLengthsEqc();
bool checkCardinality();
bool checkInductiveEquations();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback