summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorKshitij Bansal <kshitij@cs.nyu.edu>2014-09-02 18:28:52 -0400
committerKshitij Bansal <kshitij@cs.nyu.edu>2014-09-03 15:19:10 -0400
commit8dc1280a5161633fddfb8334811a86c911bb25c1 (patch)
treef4b100a3f70acc10e6ca05a1d4c28c659df0eafe /contrib
parente9fb730333b2719cddaa0a9209aa7953d7f30b0b (diff)
check() optimization
Details of testing here: http://church.cims.nyu.edu/wiki/User:Kshitij/theorycheckoptimization
Diffstat (limited to 'contrib')
-rw-r--r--contrib/theoryskel/theory_DIR.cpp3
1 files changed, 3 insertions, 0 deletions
diff --git a/contrib/theoryskel/theory_DIR.cpp b/contrib/theoryskel/theory_DIR.cpp
index 72101a5a6..535a54fd7 100644
--- a/contrib/theoryskel/theory_DIR.cpp
+++ b/contrib/theoryskel/theory_DIR.cpp
@@ -16,6 +16,9 @@ Theory$camel::Theory$camel(context::Context* c,
}/* Theory$camel::Theory$camel() */
void Theory$camel::check(Effort level) {
+ if (done() && !fullEffort(level)) {
+ return;
+ }
while(!done()) {
// Get all the assertions
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback