diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-10-09 13:22:28 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-10-09 13:22:28 +0000 |
commit | 5b65d0f80d56731fd7d07f491973bad14a85566e (patch) | |
tree | 4aafa4742804ff87408a1da7523d799851a028c0 /src/theory/model.cpp | |
parent | bdaa3049467fd17d3fb95701f7946a4bf0f5206a (diff) |
* Add assertion in TheoryModel code to ensure we don't get inconsistent
substitutions for solved variables. Related to bug 418 (and might
resolve it).
* Respect phase-locking in Minisat (one phase-saving site was unguarded).
(this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/theory/model.cpp')
-rw-r--r-- | src/theory/model.cpp | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp index 82d602017..f218332ac 100644 --- a/src/theory/model.cpp +++ b/src/theory/model.cpp @@ -260,6 +260,19 @@ Node TheoryModel::getNewDomainValue( TypeNode tn ){ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ if( !d_substitutions.hasSubstitution( x ) ){ d_substitutions.addSubstitution( x, t, invalidateCache ); + } else { +#ifdef CVC4_ASSERTIONS + Node oldX = d_substitutions.getSubstitution(x); + // check that either the old substitution is the same, or it now maps to the new substitution + if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) { + stringstream ss; + ss << "Two incompatible substitutions added to TheoryModel:\n" + << "the term: " << x << "\n" + << "old mapping: " << d_substitutions.apply(oldX) << "\n" + << "new mapping: " << d_substitutions.apply(t); + InternalError(ss.str()); + } +#endif /* CVC4_ASSERTIONS */ } } |