From b98c109f7350e5b7c9bd950e2bdee563a548636f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 29 Apr 2015 10:00:32 -0700 Subject: [PATCH] fix(kernel/hits/hits): bug in reduction rule closes #564 --- src/kernel/hits/hits.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/kernel/hits/hits.cpp b/src/kernel/hits/hits.cpp index 315e79c3f..2bfbbb3e0 100644 --- a/src/kernel/hits/hits.cpp +++ b/src/kernel/hits/hits.cpp @@ -92,6 +92,9 @@ optional> hits_normalizer_extension::operator()(expr expr const & f = args[f_pos]; expr r = mk_app(f, app_arg(mk)); + unsigned elim_arity = mk_pos+1; + if (args.size() > elim_arity) + r = mk_app(r, args.size() - elim_arity, args.begin() + elim_arity); return some_ecs(r, mk_cs.second); }