From 68174dedcb4bf9d91241585ab1cc876d2fa83d62 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 13 Mar 2019 11:37:03 -0500 Subject: Remove spurious data member. (#2857) --- src/theory/quantifiers/candidate_rewrite_database.h | 5 ----- 1 file changed, 5 deletions(-) (limited to 'src/theory') diff --git a/src/theory/quantifiers/candidate_rewrite_database.h b/src/theory/quantifiers/candidate_rewrite_database.h index 3fa9d989a..35c08f43f 100644 --- a/src/theory/quantifiers/candidate_rewrite_database.h +++ b/src/theory/quantifiers/candidate_rewrite_database.h @@ -97,11 +97,6 @@ class CandidateRewriteDatabase : public ExprMiner bool d_using_sygus; /** candidate rewrite filter */ CandidateRewriteFilter d_crewrite_filter; - /** - * Cache of skolems for each free variable that appears in a synthesis check - * (for --sygus-rr-synth-check). - */ - std::map d_fv_to_skolem; /** the cache for results of addTerm */ std::unordered_map d_add_term_cache; /** if true, we silence the output of candidate rewrites */ -- cgit v1.2.3