From 0e701138e19b960784c82812f0f9bb0ee613c2fe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 9 Dec 2015 09:53:18 -0800 Subject: [PATCH] disable restart code in seq Signed-off-by: Nikolaj Bjorner --- src/duality/duality_rpfp.cpp | 2 +- src/smt/theory_seq.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/duality/duality_rpfp.cpp b/src/duality/duality_rpfp.cpp index de3578fae..c47662ddf 100755 --- a/src/duality/duality_rpfp.cpp +++ b/src/duality/duality_rpfp.cpp @@ -670,7 +670,7 @@ namespace Duality { else { if (k == Equal && args[0].get_id() > args[1].get_id()) std::swap(args[0], args[1]); - res = f(args.size(), &args[0]); + res = f(args.size(), VEC2PTR(args)); } } else if (t.is_quantifier()) { diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d8bc522f8..d9a953154 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -660,7 +660,7 @@ void theory_seq::pop_scope_eh(unsigned num_scopes) { } void theory_seq::restart_eh() { - SASSERT(m_lhs.size() == 1); +#if 0 m.del(m_lhs.back()); m.del(m_rhs.back()); m_dam.del(m_deps.back()); @@ -670,7 +670,7 @@ void theory_seq::restart_eh() { m_lhs.push_back(expr_array()); m_rhs.push_back(expr_array()); m_deps.push_back(enode_pair_dependency_array()); - +#endif } void theory_seq::relevant_eh(app* n) {