From 0b56440cba4ce3a9a066362fd36142c7487989b7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 19 Aug 2013 19:48:09 -0700 Subject: [PATCH] fix convex converter for multi-arity addition Signed-off-by: Nikolaj Bjorner --- src/muz_qe/pdr_generalizers.cpp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/muz_qe/pdr_generalizers.cpp b/src/muz_qe/pdr_generalizers.cpp index 28226dffa..55d8a05f8 100644 --- a/src/muz_qe/pdr_generalizers.cpp +++ b/src/muz_qe/pdr_generalizers.cpp @@ -434,9 +434,19 @@ namespace pdr { if (translate(app->get_decl(), index, result)) { return true; } - if (a.is_add(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) { - result = a.mk_add(r1, r2); - return true; + if (a.is_add(term)) { + bool ok = true; + expr_ref_vector args(m); + for (unsigned i = 0; ok && i < app->get_num_args(); ++i) { + ok = mk_convex(app->get_arg(i), index, is_mul, r1); + if (ok) { + args.push_back(r1); + } + } + if (ok) { + result = a.mk_add(args.size(), args.c_ptr()); + } + return ok; } if (a.is_sub(term, e1, e2) && mk_convex(e1, index, is_mul, r1) && mk_convex(e2, index, is_mul, r2)) { result = a.mk_sub(r1, r2);