From d86a98f3a51f840c52e6b2bd52bb45e71999489f Mon Sep 17 00:00:00 2001
From: vijay_ganesh <vijay_ganesh@e59a4935-1847-0410-ae03-e826735625c1>
Date: Mon, 7 Sep 2009 19:26:10 +0000
Subject: [PATCH] emacs indentation done

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@202 e59a4935-1847-0410-ae03-e826735625c1
---
 src/AST/AbstractionRefinement.cpp | 20 ++++++++++----------
 src/AST/Transform.cpp             |  8 ++++----
 src/main/main.cpp                 | 12 ++++++------
 src/parser/let-funcs.cpp          |  4 ++--
 src/simplifier/simplifier.cpp     |  8 ++++----
 5 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/src/AST/AbstractionRefinement.cpp b/src/AST/AbstractionRefinement.cpp
index dae4a17..945c3ca 100644
--- a/src/AST/AbstractionRefinement.cpp
+++ b/src/AST/AbstractionRefinement.cpp
@@ -204,7 +204,7 @@ namespace BEEV
   
   //Creates Array Write Axioms
   ASTNode BeevMgr::Create_ArrayWriteAxioms(const ASTNode& term, 
-					   const ASTNode& newvar)
+                                           const ASTNode& newvar)
   {
     if (READ != term.GetKind() && WRITE != term[0].GetKind())
       {
@@ -241,16 +241,16 @@ namespace BEEV
                                                                  const ASTNode& original_input)
   {
     for(ASTVec::iterator i = GlobalList_Of_FiniteLoops.begin(),iend=GlobalList_Of_FiniteLoops.end();
-	i!=iend;i++)
+        i!=iend;i++)
       {
-	ASTNodeMap ParamToCurrentValMap;
-	SOLVER_RETURN_TYPE ret = SATBased_FiniteLoop_Refinement(SatSolver,
-								original_input,
-								*i,&ParamToCurrentValMap);
-	if(SOLVER_UNDECIDED != ret)
-	  {
-	    return ret;
-	  }
+        ASTNodeMap ParamToCurrentValMap;
+        SOLVER_RETURN_TYPE ret = SATBased_FiniteLoop_Refinement(SatSolver,
+                                                                original_input,
+                                                                *i,&ParamToCurrentValMap);
+        if(SOLVER_UNDECIDED != ret)
+          {
+            return ret;
+          }
       }
     return SOLVER_UNDECIDED;
   } //end of SATBased_AllFiniteLoops_Refinement()
diff --git a/src/AST/Transform.cpp b/src/AST/Transform.cpp
index 0939781..7408073 100644
--- a/src/AST/Transform.cpp
+++ b/src/AST/Transform.cpp
@@ -258,10 +258,10 @@ namespace BEEV
           break;
         }
       case FOR:
-	//Insert in a global list of FOR constructs. Return TRUE now
-	bm.GlobalList_Of_FiniteLoops.push_back(simpleForm);
-	return bm.CreateNode(TRUE);
-	break;
+        //Insert in a global list of FOR constructs. Return TRUE now
+        bm.GlobalList_Of_FiniteLoops.push_back(simpleForm);
+        return bm.CreateNode(TRUE);
+        break;
       default:
         if (k == SYMBOL && BOOLEAN_TYPE == simpleForm.GetType())
           result = simpleForm;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index d1b9f19..86da686 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -188,13 +188,13 @@ int main(int argc, char ** argv) {
   if(print_STPinput_back_flag) 
     {
       if(smtlib_parser_flag) 
-	{
-	  FatalError("Print back feature for SMT format not yet implemented\n");
-	}
+        {
+          FatalError("Print back feature for SMT format not yet implemented\n");
+        }
       else 
-	{
-	  print_STPInput_Back(asserts, query);
-	}
+        {
+          print_STPInput_Back(asserts, query);
+        }
       return 0;
     } //end of PrintBack if
 
diff --git a/src/parser/let-funcs.cpp b/src/parser/let-funcs.cpp
index fc45b30..c14de07 100644
--- a/src/parser/let-funcs.cpp
+++ b/src/parser/let-funcs.cpp
@@ -30,12 +30,12 @@ namespace BEEV {
     if(((it = _letid_expr_map->find(var)) != _letid_expr_map->end()) && 
        it->second != ASTUndefined) {      
       FatalError("LetExprMgr:The LET-var v has already been defined"\
-		 "in this LET scope: v =", var);
+                 "in this LET scope: v =", var);
     }
 
     if(_parser_symbol_table.find(var) != _parser_symbol_table.end()) {
       FatalError("LetExprMgr:This var is already declared. "\
-		 "cannot redeclare as a letvar: v =", var);
+                 "cannot redeclare as a letvar: v =", var);
     }
 
     (*_letid_expr_map)[var] = letExpr;   
diff --git a/src/simplifier/simplifier.cpp b/src/simplifier/simplifier.cpp
index aeea77b..ef0d637 100644
--- a/src/simplifier/simplifier.cpp
+++ b/src/simplifier/simplifier.cpp
@@ -47,10 +47,10 @@ namespace BEEV
     if (pushNeg && (it = SimplifyMap->find(key)) != SimplifyMap->end())
       {
         output = 
-	  (ASTFalse == it->second) ? 
-	  ASTTrue : 
-	  (ASTTrue == it->second) ? 
-	  ASTFalse : CreateNode(NOT, it->second);
+          (ASTFalse == it->second) ? 
+          ASTTrue : 
+          (ASTTrue == it->second) ? 
+          ASTFalse : CreateNode(NOT, it->second);
         CountersAndStats("2nd_Successful_CheckSimplifyMap");
         return true;
       }
-- 
2.47.3