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 /src/theory/theory_test_utils.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 'src/theory/theory_test_utils.h')
-rw-r--r-- | src/theory/theory_test_utils.h | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h index bcb1c46d7..49ed16788 100644 --- a/src/theory/theory_test_utils.h +++ b/src/theory/theory_test_utils.h @@ -81,8 +81,9 @@ public: push(PROPAGATE, n); } - void lemma(TNode n, bool removable) throw(AssertionException) { + unsigned lemma(TNode n, bool removable) throw(AssertionException) { push(LEMMA, n); + return 0; } void setIncomplete() throw(AssertionException) {} |