From 16bab71df21f60f2cdb0faab438802f7a8c66128 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Nov 2017 02:18:55 -0800
Subject: [PATCH] remove asserts for proof generation to enable mode switch in
 spacer virtual solver

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 3dbd0bc69..8c74cbe83 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -2842,21 +2842,18 @@ proof * ast_manager::mk_distributivity(expr * s, expr * r) {
 }
 
 proof * ast_manager::mk_rewrite(expr * s, expr * t) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_REWRITE, mk_eq(s, t));
 }
 
 proof * ast_manager::mk_oeq_rewrite(expr * s, expr * t) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_REWRITE, mk_oeq(s, t));
 }
 
 proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     ptr_buffer<expr> args;
@@ -2866,42 +2863,36 @@ proof * ast_manager::mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, pr
 }
 
 proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
 }
 
 proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
 }
 
 proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_PUSH_QUANT, mk_iff(q, e));
 }
 
 proof * ast_manager::mk_elim_unused_vars(quantifier * q, expr * e) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_ELIM_UNUSED_VARS, mk_iff(q, e));
 }
 
 proof * ast_manager::mk_der(quantifier * q, expr * e) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_DER, mk_iff(q, e));
 }
 
 proof * ast_manager::mk_quant_inst(expr * not_q_or_i, unsigned num_bind, expr* const* binding) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     vector<parameter> params;
@@ -2937,7 +2928,6 @@ bool ast_manager::is_rewrite(expr const* e, expr*& r1, expr*& r2) const {
 }
 
 proof * ast_manager::mk_def_axiom(expr * ax) {
-    SASSERT(proofs_enabled());
     if (proofs_disabled())
         return m_undef_proof;
     return mk_app(m_basic_family_id, PR_DEF_AXIOM, ax);