diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-13 21:20:11 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-14 01:01:10 -0500 |
| commit | e868c3d05660fe5d8dc1da8a104da850f4d101d5 (patch) | |
| tree | 2ff6ca26d11a5a03ed76eb740c413ca4a2d87f94 /test | |
| parent | 1ebd4ce25c64b1b4ea204d942512473f2ce7519c (diff) | |
Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ Google for the report and patch!
Diffstat (limited to 'test')
| -rw-r--r-- | test/system/cvc3_main.cpp | 31 |
1 files changed, 19 insertions, 12 deletions
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: " |