From bc8db289e78f3ee65728d031ecfe37f3885c4c8d Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Thu, 12 May 2016 14:01:21 +0200
Subject: [PATCH] actually verify properties for sat target
---
src/lib/CoAlgMisc.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 0332f39..8fd1f68 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -1207,6 +1207,7 @@ let ppFormulae nomTbl tbox (s, f) =
if card <= 0 then
raise (C.CoAlgException "Number of sorts must be positive.")
else ();
+ C.verifyFormula f;
let nnfAndSimplify f = C.simplify (C.nnf f) in
let f1 = nnfAndSimplify f in
let nf1 = nnfAndSimplify (C.NOT f) in
--
GitLab