smt2_solver: do not give potentially broken expressions to decision procedure

Author: Daniel Kroening

src/solvers/smt2/smt2_solver.cpp

@@ -126,7 +126,11 @@ void smt2_solvert::command(const std::string &c)
     if(c=="assert")
     {
       exprt e=expression();
-      if(e.is_not_nil())
+      if(!ok)
+      {
+        ok = true;
+      }
+      else if(e.is_not_nil())
       {
         expand_function_applications(e);
         define_constants(e);
@@ -157,7 +161,9 @@ void smt2_solvert::command(const std::string &c)
     {
       // this is a command that Z3 appears to implement
       exprt e=expression();
-      if(e.is_not_nil())
+      if(!ok)
+        ok = true;
+      else if(e.is_not_nil())
       {
         std::cout << e.pretty() << '\n'; // need to do an 'smt2_format'
       }
@@ -166,7 +172,9 @@ void smt2_solvert::command(const std::string &c)
     {
       // this is a command that Z3 appears to implement
       exprt e=expression();
-      if(e.is_not_nil())
+      if(!ok)
+        ok = true;
+      else if(e.is_not_nil())
       {
         const symbol_tablet symbol_table;
         const namespacet ns(symbol_table);