diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2012-11-14 21:54:25 +0000 |
| commit | 56013a80a76b0d46f6f8497d7570e51877dbf99d (patch) | |
| tree | 9d4ed01590a15b13b91485333fd497e26889e0c0 /src/theory/model.h | |
| parent | b273e586629c5759dc88cd962e52a89f65b674a7 (diff) | |
bug fixes to models, array rewriter with previously failing testcases
Diffstat (limited to 'src/theory/model.h')
| -rw-r--r-- | src/theory/model.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 5b691d4d9..d17192281 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -92,7 +92,7 @@ public: /** assert predicate holds in the model */ void assertPredicate( Node a, bool polarity ); /** assert all equalities/predicates in equality engine hold in the model */ - void assertEqualityEngine( const eq::EqualityEngine* ee ); + void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL); /** assert representative * This function tells the model that n should be the representative of its equivalence class. * It should be called during model generation, before final representatives are chosen. In the |