From 9554723b44860733e8a633de724aa06bb9ed9a99 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 6 Dec 2017 20:50:03 -0500 Subject: [PATCH] use safer mk_and in extended indexof --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index a931ae458..4f84ed2f7 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1330,7 +1330,7 @@ namespace smt { ite2ElseItems.push_back(ctx.mk_eq_atom(indexAst, mk_indexof(suffix, expr->get_arg(1)))); ite2ElseItems.push_back(ctx.mk_eq_atom(expr->get_arg(2), prefixLen)); ite2ElseItems.push_back(ite3); - expr_ref ite2Else(m.mk_and(ite2ElseItems.size(), ite2ElseItems.c_ptr()), m); + expr_ref ite2Else(mk_and(ite2ElseItems), m); SASSERT(ite2Else); expr_ref ite2(m.mk_ite(