From 89c9bb2e0e5867ec858a30374ef4411f4ccfd1ac Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 29 Nov 2019 17:19:26 -0500 Subject: [PATCH] z3str3: don't call propagate() in init_search_eh() --- src/smt/theory_str.cpp | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 111304c3c..4b36ad501 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7748,10 +7748,6 @@ namespace smt { set_up_axioms(ex); } - // this might be cheating but we need to make sure that certain maps are populated - // before the first call to new_eq_eh() - propagate(); - TRACE("str", tout << "search started" << std::endl;); search_started = true; }