From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 14 Nov 2013 02:20:11 +0000 (-0500)
Subject: Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ Google... 
X-Git-Tag: cvc5-1.0.0~7252
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e868c3d05660fe5d8dc1da8a104da850f4d101d5;p=cvc5.git

Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ Google for the report and patch!
---

diff --git a/test/system/cvc3_main.cpp b/test/system/cvc3_main.cpp
index 69d29d1da..641eae725 100644
--- a/test/system/cvc3_main.cpp
+++ b/test/system/cvc3_main.cpp
@@ -33,6 +33,7 @@
 //#include "theory_array.h"
 #include <fstream>
 #include <iostream>
+#include <sstream>
 #include <string>
 #include <deque>
 //#include "exception.h"
@@ -70,13 +71,10 @@ bool check(ValidityChecker* vc, Expr e, bool verbose=true)
     vc->printExpr(e);
   }
   bool res = vc->query(e);
-  switch (res) {
-    case false:
-      if(verbose) cout << "Invalid" << endl << endl;
-      break;
-    case true:
-      if(verbose) cout << "Valid" << endl << endl;
-      break;
+  if (res) {
+    if(verbose) cout << "Valid" << endl << endl;
+  } else {
+    if(verbose) cout << "Invalid" << endl << endl;
   }
   return res;
 }
@@ -1923,30 +1921,39 @@ void test22() {
 
     Expr s(vc->exprFromString("FORALL (x:INT) : x > f(x)"));
     vc->setTrigger(s,fx);
-    
+
+    std::ostringstream stringHolder("");
     std::vector<std::vector<Expr> > trigsvv = s.getTriggers();
+    stringHolder << trigsvv.size();
     EXPECT( trigsvv.size() == 1, 
-                 "Expected s.getTriggers().size() == 1: " + trigsvv.size() );
+                 "Expected s.getTriggers().size() == 1: " + stringHolder.str() );
 
+    stringHolder.str("");
     std::vector<Expr> trigsv = trigsvv[0];
+    stringHolder << trigsv.size();
+
     EXPECT( trigsv.size() == 1, 
                  "Expected s.getTriggers()[0].size() == 1: "
-                 + trigsv.size() );
+                 + stringHolder.str() );
 
     EXPECT( trigsv[0] == fx, 
                  "Expected s.getTriggers()[0][0] == fx: "
                  + (trigsv[0].toString()) );
 
+    stringHolder.str("");
     Expr t(vc->exprFromString("FORALL (x:INT) : x > f(x)"));
     vc->setMultiTrigger(t,patternv);
     trigsvv = t.getTriggers();
+    stringHolder << trigsvv.size();
     EXPECT( trigsvv.size() == 1,
-                 "Expected t.getTriggers().size() == 1: " + trigsvv.size() );
+                 "Expected t.getTriggers().size() == 1: " + stringHolder.str() );
 
+    stringHolder.str("");
     trigsv = trigsvv[0];
+    stringHolder << trigsv.size();
     EXPECT( trigsv.size() == 1,
                  "Expected t.getTriggers()[0].size() == 1: "
-                 + trigsv.size() );
+                 + stringHolder.str() );
 
     EXPECT( trigsv[0] == fx,
                  "Expected t.getTriggers()[0][0] == fx: "