From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 16 Dec 2014 23:04:47 +0000 (-0500)
Subject: Fix oversight in dumping assertions in preprocessing.
X-Git-Tag: cvc5-1.0.0~6461
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=92d9c961aeb90531ca56d4014f4679d0241a6148;p=cvc5.git

Fix oversight in dumping assertions in preprocessing.
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 659051725..918d6f30d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2707,6 +2707,8 @@ bool SmtEnginePrivate::simplifyAssertions()
 
     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
 
+    dumpAssertions("pre-nonclausal", d_assertions);
+
     if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
       // Perform non-clausal simplification
       Chat() << "...performing nonclausal simplification..." << endl;