From 1ed4aa391c5919476175c46000bd6ce06e58835d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 20 Dec 2013 14:14:15 -0800 Subject: [PATCH] fix(library/fo_unify): bug at function that extracts the lhs and rhs of homogeneous/heterogeneous equality For homogeneous equality, arg #1 is the Type of the lhs/rhs. Signed-off-by: Leonardo de Moura --- src/library/fo_unify.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/fo_unify.cpp b/src/library/fo_unify.cpp index 6c8a90954..f2088a346 100644 --- a/src/library/fo_unify.cpp +++ b/src/library/fo_unify.cpp @@ -29,7 +29,7 @@ static expr_pair eq_heq_args(expr const & e) { if (is_eq(e)) return expr_pair(eq_lhs(e), eq_rhs(e)); else - return expr_pair(arg(e, 1), arg(e, 2)); + return expr_pair(arg(e, 2), arg(e, 3)); } optional fo_unify(expr e1, expr e2) {