diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-10-23 00:45:57 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-10-23 00:45:57 +0000 |
| commit | 18f710cbfb5ce1ea13c8e929445abc211c732a81 (patch) | |
| tree | 69e4517ad67d6afd82c4b48a886e828ed84070f1 /test/unit/theory/theory_black.h | |
| parent | 9039185001b789eadd8b20149455fe778a80fb69 (diff) | |
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.
Diffstat (limited to 'test/unit/theory/theory_black.h')
| -rw-r--r-- | test/unit/theory/theory_black.h | 3 |
1 files changed, 2 insertions, 1 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() |