From d72790e5c62ff9732b2f67990de44e0412a3eba5 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 13 Apr 2011 12:58:34 +0000 Subject: [PATCH] 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 --- src/to-sat/AIG/ToSATAIG.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/to-sat/AIG/ToSATAIG.cpp b/src/to-sat/AIG/ToSATAIG.cpp index 2d42c37..011e5b2 100644 --- 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); } -- 2.47.3