TV: don't stop on invalid SMT expressions
MODIFY
tv/tv.cpp
tv/tv.cpp
@@ -125,6 +125,7 @@ struct TVPass : public llvm::FunctionPass {
*out << "Transformation doesn't verify!\n" << errs << endl;
if (opt_error_fatal &&
!errs.isTimeout() &&
+ !errs.isInvalidExpr() &&
!errs.isOOM() &&
!errs.isLoopyCFG())
llvm::report_fatal_error("Alive2: Transform doesn't verify; aborting!");

MODIFY
util/errors.cpp
util/errors.cpp
@@ -27,6 +27,10 @@ bool Errors::isTimeout() const {
return errs.size() == 1 && errs[0] == "Timeout";
}
+bool Errors::isInvalidExpr() const {
+ return errs.size() == 1 && errs[0] == "Invalid expr";
+}
+
bool Errors::isOOM() const {
return errs.size() == 1 && errs[0] == "Out of memory; skipping function.";
}

MODIFY
util/errors.h
util/errors.h
@@ -20,6 +20,7 @@ public:
void add(std::string &&str);
explicit operator bool() const { return !errs.empty(); }
bool isTimeout() const;
+ bool isInvalidExpr() const;
bool isOOM() const;
bool isLoopyCFG() const; // FIXME

TV: don't stop on invalid SMT expressions