summaryrefslogtreecommitdiff
path: root/src/theory/theory_test_utils.h
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2012-06-06 06:12:40 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2012-06-06 06:12:40 +0000
commitfd9e22c4a2e57c3dfeda4de3842a3fb3ca4776ba (patch)
tree047e4d27f725e9157ed5bef5357d0d72560218ae /src/theory/theory_test_utils.h
parent2799ae1cf57ed2b98387a1de1325bccd89bd2a30 (diff)
Changes to the combination mechanism, lots of details. Not done yet, there are still the AUFBV wrong results, but it seems better.
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4382&reference_id=4359&p=5
Diffstat (limited to 'src/theory/theory_test_utils.h')
-rw-r--r--src/theory/theory_test_utils.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/theory_test_utils.h b/src/theory/theory_test_utils.h
index aaf47425b..bf1370090 100644
--- a/src/theory/theory_test_utils.h
+++ b/src/theory/theory_test_utils.h
@@ -78,9 +78,10 @@ public:
push(CONFLICT, n);
}
- void propagate(TNode n)
+ bool propagate(TNode n)
throw(AssertionException) {
push(PROPAGATE, n);
+ return true;
}
void propagateAsDecision(TNode n)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback