From 247c570e6b35e5ac8dc680e71eaa2ad0a8dae308 Mon Sep 17 00:00:00 2001
From: Bernhard Gleiss <bgleiss@forsyte.tuwien.ac.at>
Date: Mon, 27 Nov 2017 16:46:14 +0100
Subject: [PATCH] Debug sanity check in spacer_context

Triggered by bugs in hypothesis remover

only sanitycheck lemmas in debug-mode
---
 src/muz/spacer/spacer_context.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 75a9d7d81..f700ce83e 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -3133,7 +3133,12 @@ lbool context::expand_node(pob& n)
             checkpoint ();
             (*m_lemma_generalizers[i])(lemma);
         }
+        DEBUG_CODE(
+                   lemma_sanity_checker sanity_checker(*this);
+                   sanity_checker(lemma);
+                   );
 
+        
         TRACE("spacer", tout << "invariant state: "
               << (is_infty_level(lemma->level())?"(inductive)":"")
               <<  mk_pp(lemma->get_expr(), m) << "\n";);