Implement changes from yesterday morning's meeting (10/21/2011):

* OutputChannel::lemma() now returns an unsigned int.  This facility isn't functional yet, but the signature is there.  For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want).
* Pseudobooleans disabled.  This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch.
* --limit / --time-limit options renamed --rlimit and --tlimit.

There may be slowdown from disabling pseudobooleans.

2 files changed, 3 insertions, 2 deletions

diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h
index be1d4a35b..e5577d2c2 100644
--- a/test/unit/theory/theory_black.h
+++ b/test/unit/theory/theory_black.h
@@ -62,9 +62,10 @@ public:
     push(PROPAGATE, n);
   }
 
-  void lemma(TNode n, bool removable)
+  unsigned lemma(TNode n, bool removable)
     throw(AssertionException) {
     push(LEMMA, n);
+    return 0;
   }
 
   void setIncomplete()
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index 7132d9b17..fbac6f4ee 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -54,7 +54,7 @@ class FakeOutputChannel : public OutputChannel {
   void propagate(TNode n) throw(AssertionException) {
     Unimplemented();
   }
-  void lemma(TNode n, bool removable) throw(AssertionException) {
+  unsigned lemma(TNode n, bool removable) throw(AssertionException) {
     Unimplemented();
   }
   void explanation(TNode n) throw(AssertionException) {