diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-03 19:16:39 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-04-03 19:38:21 -0400 |
| commit | 428572ea18afa8fdcaaedfa0c293182cf5a00a3d (patch) | |
| tree | 34c0fe0547e3aea8c5ef67f0ba3afc8d55df2500 /src/smt/boolean_terms.cpp | |
| parent | e99ed158fb2c5e030f38d048d2b2f2be6b11c7fb (diff) | |
Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue.
Diffstat (limited to 'src/smt/boolean_terms.cpp')
| -rw-r--r-- | src/smt/boolean_terms.cpp | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index c1596dddc..4555aac51 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -43,8 +43,8 @@ BooleanTermConverter::BooleanTermConverter(SmtEngine& smt) : d_tt(), d_ffDt(), d_ttDt(), - d_varCache(), - d_termCache(), + d_varCache(smt.d_userContext), + d_termCache(smt.d_userContext), d_typeCache(), d_datatypeCache() { @@ -640,7 +640,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa if(dt != dt2) { Assert(d_varCache.find(top) != d_varCache.end(), "constructor `%s' not in cache", top.toString().c_str()); - result.top() << d_varCache[top]; + result.top() << d_varCache[top].get(); worklist.pop(); goto next_worklist; } @@ -658,7 +658,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa if(dt != dt2) { Assert(d_varCache.find(top) != d_varCache.end(), "tester or selector `%s' not in cache", top.toString().c_str()); - result.top() << d_varCache[top]; + result.top() << d_varCache[top].get(); worklist.pop(); goto next_worklist; } else { |