From f9b3c47bf513672f0dcf76c202e8cd7d6b509aa1 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 14 Feb 2017 18:45:09 -0500 Subject: [PATCH] remove commented-out old worklists --- src/smt/theory_str.h | 15 +-------------- 1 file changed, 1 insertion(+), 14 deletions(-) diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 1915763f1..47a8e8d0b 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -209,20 +209,7 @@ namespace smt { ptr_vector m_string_constant_length_todo; ptr_vector m_concat_eval_todo; - // enode lists for term-specific axioms - /* - ptr_vector m_axiom_CharAt_todo; - ptr_vector m_axiom_StartsWith_todo; - ptr_vector m_axiom_EndsWith_todo; - ptr_vector m_axiom_Contains_todo; - ptr_vector m_axiom_Indexof_todo; - ptr_vector m_axiom_Indexof2_todo; - ptr_vector m_axiom_LastIndexof_todo; - ptr_vector m_axiom_Substr_todo; - ptr_vector m_axiom_Replace_todo; - ptr_vector m_axiom_RegexIn_todo; - */ - + // enode lists for library-aware/high-level string terms (e.g. substr, contains) ptr_vector m_library_aware_axiom_todo; // hashtable of all exprs for which we've already set up term-specific axioms --