From 45228bf8fb2c3bc07abade538b8f5d64f4a3a067 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 20 Jun 2021 09:25:02 -0700 Subject: [PATCH] #5323 heap use after free Signed-off-by: Nikolaj Bjorner --- src/qe/mbp/mbp_arith.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index fb07ae450..ab13e0813 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -283,7 +283,8 @@ namespace mbp { unsigned j = 0; TRACE("qe", tout << "vars: " << vars << "\nfmls: " << fmls << "\n"; for (expr* f : fmls) tout << mk_pp(f, m) << " := " << model(f) << "\n";); - for (expr* fml : fmls) { + for (unsigned i = 0; i < fmls.size(); ++i) { + expr* fml = fmls.get(i); if (!linearize(mbo, eval, fml, fmls, tids)) { TRACE("qe", tout << "could not linearize: " << mk_pp(fml, m) << "\n";); fmls[j++] = fml;