From 428572ea18afa8fdcaaedfa0c293182cf5a00a3d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 3 Apr 2014 19:16:39 -0400 Subject: Some incremental bugs for Boolean terms, fixed. Thanks to Pantazis Deligiannis and Jeroen Ketema for discovering this issue. --- src/smt/boolean_terms.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/smt/boolean_terms.cpp') 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 { -- cgit v1.2.3