After resolving conflicts

diff --cc src/AST/element.h
index 1b790848518c7a146707fc9a51627051d89cef02,b74e582630d594d22708e1114442ed4cba3310ee..1e7b1f2899aaba7883573adab92c09b923ad5d79
--- 1/src/AST/element.h
--- 2/src/AST/element.h
+++ b/src/AST/element.h
@@@ -26,14 -26,13 +26,14 @@@ public
  class ElementSet : public Element {
  public:
        ElementSet(ASTNodeType type, Set *s);
 +        virtual ~ElementSet(){}
        ElementSet(Set *s);
        virtual Element *clone(CSolver *solver, CloneMap *map);
-       virtual void serialize(Serializer* serializer);
-         virtual void print();
+       virtual void serialize(Serializer *serializer);
+       virtual void print();
        CMEMALLOC;
        Set *getRange() {return set;}
-  protected:
+ protected:
        Set *set;
  
  };
@@@ -41,10 -40,9 +41,10 @@@
  class ElementConst : public ElementSet {
  public:
        ElementConst(uint64_t value, Set *_set);
 +        virtual ~ElementConst(){}
        uint64_t value;
-       virtual void serialize(Serializer* serializer);
-         virtual void print();
+       virtual void serialize(Serializer *serializer);
+       virtual void print();
        Element *clone(CSolver *solver, CloneMap *map);
        CMEMALLOC;
  };

diff --cc src/AST/set.cc
index 5c07ac5ce49ef59b37a431bd19d5e613e7759daf,0a6e14f41a95dfdf439fa3ef06153083f67ccff2..52494e393ca9ef682fbd5d20bce9e52041d31665
--- 1/src/AST/set.cc
--- 2/src/AST/set.cc
+++ b/src/AST/set.cc
@@@ -127,36 -135,33 +135,36 @@@ void Set::serialize(Serializer *seriali
        serializer->addObject(this);
        ASTNodeType asttype = SETTYPE;
        serializer->mywrite(&asttype, sizeof(ASTNodeType));
-       Set* This = this;
-       serializer->mywrite(&This, sizeof(Set*));
+       Set *This = this;
+       serializer->mywrite(&This, sizeof(Set *));
        serializer->mywrite(&type, sizeof(VarType));
        serializer->mywrite(&isRange, sizeof(bool));
 -      serializer->mywrite(&low, sizeof(uint64_t));
 -      serializer->mywrite(&high, sizeof(uint64_t));
 -      bool isMutable = isMutableSet();
 +        bool isMutable = isMutableSet();
        serializer->mywrite(&isMutable, sizeof(bool));
 -      uint size = members->getSize();
 -      serializer->mywrite(&size, sizeof(uint));
 -      for (uint i = 0; i < size; i++) {
 -              uint64_t mem = members->get(i);
 -              serializer->mywrite(&mem, sizeof(uint64_t));
 -      }
 +        if(isRange){
 +                serializer->mywrite(&low, sizeof(uint64_t));
 +                serializer->mywrite(&high, sizeof(uint64_t));
 +        }else {
 +                uint size = members->getSize();
 +                serializer->mywrite(&size, sizeof(uint));
 +                for(uint i=0; i<size; i++){
 +                        uint64_t mem = members->get(i);
 +                        serializer->mywrite(&mem, sizeof(uint64_t));
 +                }
 +        }
  }
  
- void Set::print(){
+ void Set::print() {
        model_print("{Set:");
-         if(isRange){
-                 model_print("Range: low=%lu, high=%lu}\n\n", low, high);
-         } else {
-                 uint size = members->getSize();
-                 model_print("Members: ");
-                 for(uint i=0; i<size; i++){
-                         uint64_t mem = members->get(i);
-                         model_print("%lu, ", mem);
-                 }
-                 model_println("}\n");
-         }
+       if (isRange) {
+               model_print("Range: low=%lu, high=%lu}", low, high);
+       } else {
+               uint size = members->getSize();
+               model_print("Members: ");
+               for (uint i = 0; i < size; i++) {
+                       uint64_t mem = members->get(i);
+                       model_print("%lu, ", mem);
+               }
+               model_print("}");
+       }
  }

diff --cc src/Serialize/deserializer.cc
index bffb901153216f812f6797d3265618e5c48b4196,cd1e1a232fca290d3401e140e96854bbaf1dfbbb..6f14484c95646b2da6752ef9cb77e8d2fa27b437
--- 1/src/Serialize/deserializer.cc
--- 2/src/Serialize/deserializer.cc
+++ b/src/Serialize/deserializer.cc
@@@ -145,40 -145,36 +145,39 @@@ void Deserializer::deserializeSet() 
        myread(&type, sizeof(VarType));
        bool isRange;
        myread(&isRange, sizeof(bool));
 -      uint64_t low;
 -      myread(&low, sizeof(uint64_t));
 -      uint64_t high;
 -      myread(&high, sizeof(uint64_t));
 -      bool isMutable;
 +        bool isMutable;
        myread(&isMutable, sizeof(bool));
 -      Set *set;
 -      if (isMutable) {
 -              set = new MutableSet(type);
 -      }
 -      uint size;
 -      myread(&size, sizeof(uint));
 -      Vector<uint64_t> members;
 -      for (uint i = 0; i < size; i++) {
 -              uint64_t mem;
 -              myread(&mem, sizeof(uint64_t));
 -              if (isMutable) {
 -                      ((MutableSet *) set)->addElementMSet(mem);
 -              } else {
 -                      members.push(mem);
 -              }
 -      }
 -      if (!isMutable) {
 -              set = isRange ? solver->createRangeSet(type, low, high) :
 -                                      solver->createSet(type, members.expose(), size);
 -      }
 -      map.put(s_ptr, set);
 +        if(isRange){
 +                uint64_t low;
 +                myread(&low, sizeof(uint64_t));
 +                uint64_t high;
 +                myread(&high, sizeof(uint64_t));
 +                map.put(s_ptr, new Set(type, low, high));
 +        } else{
 +                Set *set;
 +                if(isMutable){
 +                        set = new MutableSet(type);
 +                }
 +                uint size;
 +                myread(&size, sizeof(uint));
 +                Vector<uint64_t> members;
 +                for(uint i=0; i<size; i++){
 +                        uint64_t mem;
 +                        myread(&mem, sizeof(uint64_t));
 +                        if(isMutable) {
 +                                ((MutableSet*) set)->addElementMSet(mem);
 +                        }else {
 +                                members.push(mem);
 +                        }
 +                }
 +                if(!isMutable){
 +                        set = solver->createSet(type, members.expose(), size);
 +                }
 +                map.put(s_ptr, set);
 +        }
-       
  }
  
- void Deserializer::deserializeBooleanLogic(){
+ void Deserializer::deserializeBooleanLogic() {
        BooleanLogic *bl_ptr;
        myread(&bl_ptr, sizeof(BooleanLogic *));
        LogicOp op;
@@@ -376,15 -372,15 +375,15 @@@ void Deserializer::deserializeFunctionO
        map.put(fo_ptr, solver->createFunctionOperator(op, domains.expose(), size, range, overflowbehavior));
  }
  
- void Deserializer::deserializeFunctionTable(){
+ void Deserializer::deserializeFunctionTable() {
        FunctionTable *ft_ptr;
        myread(&ft_ptr, sizeof(FunctionTable *));
-       Table* table;
-       myread(&table, sizeof(Table*));
+       Table *table;
+       myread(&table, sizeof(Table *));
        ASSERT(map.contains(table));
-       table = (Table*) map.get(table);
+       table = (Table *) map.get(table);
        UndefinedBehavior undefinedbehavior;
        myread(&undefinedbehavior, sizeof(UndefinedBehavior));
-       
+ 
        map.put(ft_ptr, solver->completeTable(table, undefinedbehavior));
--}
++}

diff --cc src/common.h
index fac5a0bef27eaded2e5993406bf8c7a30d7c51ee,52c0b5f7ebd85b9e0830bafee33367b18bc19123..0efebf8152d581e20066ca2e32222b5be37e9717
--- 1/src/common.h
--- 2/src/common.h
+++ b/src/common.h
@@@ -18,20 -18,22 +18,23 @@@
  #include "config.h"
  #include "time.h"
  
 -/*
 -   extern int model_out;
 -   extern int model_err;
 -   extern int switch_alloc;
+ 
 - #define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
 - #define model_print(fmt, ...) do { printf(fmt, ## __VA_ARGS__); } while (0)
 - #define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
 +#if 1
 +extern int model_out;
 +extern int model_err;
 +extern int switch_alloc;
  
 - #define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
 +#define model_dprintf(fd, fmt, ...) do { switch_alloc = 1; dprintf(fd, fmt, ## __VA_ARGS__); switch_alloc = 0; } while (0)
 +
 +#define model_print(fmt, ...) do { model_dprintf(model_out, fmt, ## __VA_ARGS__); } while (0)
 +#define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
 +#else
 +    #define model_print printf
 +#endif
 +#define model_println(fmt, ...) do { model_print(fmt, ## __VA_ARGS__); model_print("\n");} while(0)
  
 - #define model_print_err(fmt, ...) do { model_dprintf(model_err, fmt, ## __VA_ARGS__); } while (0)
 - */
+ 
 -#define model_print printf
+ 
  #define NEXTPOW2(x) ((x == 1) ? 1 : (1 << (sizeof(uint) * 8 - __builtin_clz(x - 1))))
  #define NUMBITS(x) ((x == 0) ? 0 : 8 * sizeof(x) - __builtin_clz(x))
  

diff --cc src/csolver.cc
index d2e44b4fcd6030b981cc65209030bba8e9c92af1,311ad0f5052ac00ac29ff03cbdbc1082912fcd94..81329914c80acea519b310c0bad122328876aff8
--- 1/src/csolver.cc
--- 2/src/csolver.cc
+++ b/src/csolver.cc
@@@ -101,12 -98,12 +101,11 @@@ void CSolver::serialize() 
                }
                delete it;
        }
 -      model_print("deserializing ...\n");
 -      {
 -              Deserializer deserializer("dump");
 -              deserializer.deserialize();
 -      }
 -
 +//    model_print("deserializing ...\n");
 +//    {
 +//            Deserializer deserializer("dump");
 +//            deserializer.deserialize();
 +//    }
-       
  }
  
  Set *CSolver::createSet(VarType type, uint64_t *elements, uint numelements) {
@@@ -417,27 -393,18 +398,21 @@@ BooleanEdge CSolver::orderConstraint(Or
  }
  
  void CSolver::addConstraint(BooleanEdge constraint) {
 +#ifdef TRACE_DEBUG
 +        model_println("****New Constraint******");
 +#endif
        if (isTrue(constraint))
                return;
-       else if (isFalse(constraint)){
-                 int t=0;
- #ifdef TRACE_DEBUG
-               model_println("Adding constraint which is false :|");
- #endif
-                 setUnSAT();
-         }
+       else if (isFalse(constraint)) {
+               int t = 0;
+               setUnSAT();
+       }
        else {
                if (constraint->type == LOGICOP) {
-                       BooleanLogic *b=(BooleanLogic *) constraint.getBoolean();
+                       BooleanLogic *b = (BooleanLogic *) constraint.getBoolean();
                        if (!constraint.isNegated()) {
-                               if (b->op==SATC_AND) {
-                                       for(uint i=0;i<b->inputs.getSize();i++) {
- #ifdef TRACE_DEBUG
-                                                 model_println("In loop");
- #endif
+                               if (b->op == SATC_AND) {
+                                       for (uint i = 0; i < b->inputs.getSize(); i++) {
                                                addConstraint(b->inputs.get(i));
                                        }
                                        return;