Improvement. Add a warning message when using --exit-after-CNF with arrays, without -r.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1273 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp
index 2d42c37f3b0ebb201f430a14f493559cd2da4630..011e5b2eb1389a74a08bd51654c58130d07f7e42 100644 (file)
--- a/src/to-sat/AIG/ToSATAIG.cpp
+++ b/src/to-sat/AIG/ToSATAIG.cpp
@@ -123,6 +123,12 @@ namespace BEEV
       {
         if (bm->UserFlags.quick_statistics_flag)
           bm->GetRunTimes()->print();
+
+        if (needAbsRef)
+          cerr << "Warning: STP is exiting after generating the first CNF. But the CNF"
+          "is probably partial which you probably don't want. You probably want to disable"
+          "refinement with the \"-r\" command line option." << endl;
+
         exit(0);
       }