From 96d27b6b8fd2b125ecc5a38554420e46ca2b64ef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 10 Sep 2016 12:13:31 -0700 Subject: [PATCH] fix(library/equations_compiler/elim_match): missing case for is_complete_transition --- src/library/equations_compiler/elim_match.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/library/equations_compiler/elim_match.cpp b/src/library/equations_compiler/elim_match.cpp index b116e52051..41e685244d 100644 --- a/src/library/equations_compiler/elim_match.cpp +++ b/src/library/equations_compiler/elim_match.cpp @@ -479,7 +479,7 @@ struct elim_match_fn { /* Return true iff the next pattern of every equation is a constructor or variable, and there are at least one equation where it is a variable and another where it is a constructor. */ - bool is_complete_transition(problem const & P) const { + bool is_complete_transition(problem const & P) { bool has_variable = false; bool has_constructor = false; bool r = all_next_pattern(P, [&](expr const & p) { @@ -487,6 +487,8 @@ struct elim_match_fn { has_variable = true; return true; } else if (is_constructor_app(p)) { has_constructor = true; return true; + } else if (is_value(p)) { + return true; } else { return false; }