From 050104cdfda29f303c403c288686a7641eb7edb5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 2 Dec 2014 12:17:59 -0800
Subject: [PATCH] fix(library/unifier): assertion violation

---
 src/library/unifier.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp
index 67c296d91c..6ee42ed617 100644
--- a/src/library/unifier.cpp
+++ b/src/library/unifier.cpp
@@ -2191,7 +2191,7 @@ struct unifier_fn {
         constraint c   = p->first;
         unsigned cidx  = p->second;
         if (cidx >= get_group_first_index(cnstr_group::ClassInstance) &&
-            !m_config.m_discard && cnstr_on_demand(c)) {
+            !m_config.m_discard && is_choice_cnstr(c) && cnstr_on_demand(c)) {
             // we postpone class-instance constraints whose type still contains metavariables
             m_cnstrs.erase_min();
             postpone(c);