Skip to content
This repository has been archived by the owner on Oct 14, 2023. It is now read-only.

Commit

Permalink
fix(library/fo_unify): bug at function that extracts the lhs and rhs …
Browse files Browse the repository at this point in the history
…of homogeneous/heterogeneous equality

For homogeneous equality, arg #1 is the Type of the lhs/rhs.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
  • Loading branch information
leodemoura committed Dec 20, 2013
1 parent 7772c16 commit 1ed4aa3
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/library/fo_unify.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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<substitution> fo_unify(expr e1, expr e2) {
Expand Down

0 comments on commit 1ed4aa3

Please sign in to comment.