]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
Bugfix. Save the value of print counter example as per the bug report from Markus...
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 14 Jun 2010 04:06:32 +0000 (04:06 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 14 Jun 2010 04:06:32 +0000 (04:06 +0000)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@842 e59a4935-1847-0410-ae03-e826735625c1

src/c_interface/c_interface.cpp

index 7e71f46238e409185b3f83f5e672ebefb4c67279..fc6111ca50730cba7e2bf0e8b9cb3967b2b22545 100644 (file)
@@ -352,10 +352,12 @@ void vc_printCounterExampleToBuffer(VC vc, char **buf, unsigned long *len) {
 
   // formate the state of the query
   std::ostringstream os;
+  bool currentPrint = b->UserFlags.print_counterexample_flag;
   b->UserFlags.print_counterexample_flag = true;
   os << "COUNTEREXAMPLE BEGIN: \n";
   ce->PrintCounterExample(true,os);
   os << "COUNTEREXAMPLE END: \n";
+  b->UserFlags.print_counterexample_flag = currentPrint;
 
   // convert to a c buffer
   string s = os.str();
@@ -572,10 +574,12 @@ void vc_printCounterExample(VC vc) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);
 
-  b->UserFlags.print_counterexample_flag = true;
+  bool currentPrint = b->UserFlags.print_counterexample_flag;
+    b->UserFlags.print_counterexample_flag = true;
   cout << "COUNTEREXAMPLE BEGIN: \n";
   ce->PrintCounterExample(true);
   cout << "COUNTEREXAMPLE END: \n";
+  b->UserFlags.print_counterexample_flag = currentPrint;
 }
 
 // //! Return the counterexample after a failed query.
@@ -1946,10 +1950,12 @@ void vc_printCounterExampleFile(VC vc, int fd) {
   bmstar b = (bmstar)(((stpstar)vc)->bm);
   ctrexamplestar ce = (ctrexamplestar)(((stpstar)vc)->Ctr_Example);  
   
+  bool currentPrint = b->UserFlags.print_counterexample_flag;
   b->UserFlags.print_counterexample_flag = true;
   os << "COUNTEREXAMPLE BEGIN: \n";
   ce->PrintCounterExample(true, os);
   os << "COUNTEREXAMPLE END: \n";
+  b->UserFlags.print_counterexample_flag = currentPrint;
 }
 
 const char* exprName(Expr e){