cleaned out decision_proceduret::D_TAUTOLOGY

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3862 6afb6bc1-c8e4-404c-8f48-9ae832c5b171

Author: kroening

src/path-symex/path_symex_state.cpp

@@ -695,7 +695,6 @@ bool path_symex_statet::is_feasible(
   // check whether SAT
   switch(decision_procedure())
   {
-  case decision_proceduret::D_TAUTOLOGY:
   case decision_proceduret::D_SATISFIABLE: return true;
 
   case decision_proceduret::D_UNSATISFIABLE: return false;
@@ -741,7 +740,6 @@ bool path_symex_statet::check_assertion(
   // check whether SAT  
   switch(decision_procedure.dec_solve())
   {
-  case decision_proceduret::D_TAUTOLOGY:
   case decision_proceduret::D_SATISFIABLE:
     return false; // error
 

src/util/decision_procedure.h

@@ -39,8 +39,7 @@ class decision_proceduret:public messaget
   { set_to(expr, false); }
 
   // solve the problem
-  typedef enum { D_TAUTOLOGY, D_SATISFIABLE,
-                 D_UNSATISFIABLE, D_ERROR } resultt;
+  typedef enum { D_SATISFIABLE, D_UNSATISFIABLE, D_ERROR } resultt;
 
   // will eventually be protected, use below call operator  
   virtual resultt dec_solve()=0;