From f145ceecb408b4e8ef9253d30ba0fd1d3126b364 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 8 Jul 2015 22:12:41 -0700
Subject: [PATCH] remove default failure on proof mode fixes #121

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/tactic/arith/card2bv_tactic.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/tactic/arith/card2bv_tactic.cpp b/src/tactic/arith/card2bv_tactic.cpp
index 465173196..b4be4b862 100644
--- a/src/tactic/arith/card2bv_tactic.cpp
+++ b/src/tactic/arith/card2bv_tactic.cpp
@@ -473,7 +473,6 @@ public:
                             expr_dependency_ref & core) {
         TRACE("card2bv-before", g->display(tout););
         SASSERT(g->is_well_sorted());
-        fail_if_proof_generation("card2bv", g);
         mc = 0; pc = 0; core = 0; result.reset();
         tactic_report report("card2bv", *g);
         m_rw1.reset();