From 2239791eab4ebabe85b0319e36851650dfafc080 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 Jan 2017 18:55:45 -0800 Subject: [PATCH] fix(library/tactic/smt/congruence_closure): typo --- src/library/tactic/smt/congruence_closure.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/tactic/smt/congruence_closure.cpp b/src/library/tactic/smt/congruence_closure.cpp index b5691c0a75..8cf32699dc 100644 --- a/src/library/tactic/smt/congruence_closure.cpp +++ b/src/library/tactic/smt/congruence_closure.cpp @@ -1914,7 +1914,7 @@ void initialize_congruence_closure() { g_or_eq_of_eq_false_right = new expr(mk_constant("or_eq_of_eq_false_right")); g_or_eq_of_eq = new expr(mk_constant("or_eq_of_eq")); - g_not_eq_of_eq_true = new expr(mk_constant("not_eq_of_eq_true ")); + g_not_eq_of_eq_true = new expr(mk_constant("not_eq_of_eq_true")); g_not_eq_of_eq_false = new expr(mk_constant("not_eq_of_eq_false")); g_false_of_a_eq_not_a = new expr(mk_constant("false_of_a_eq_not_a"));