diff --git a/include/klee/Module/KType.h b/include/klee/Module/KType.h
index 6115c6ac9b..755c5a06fa 100644
--- a/include/klee/Module/KType.h
+++ b/include/klee/Module/KType.h
@@ -36,6 +36,16 @@ class KType {
    */
   TypeManager *parent;
 
+  /**
+   * Alignment in bytes for this type.
+   */
+  size_t alignment = 1;
+
+  /**
+   * Size of type.
+   */
+  size_t typeStoreSize = 0;
+
   /**
    * Innner types. Maps type to their offsets in current
    * type. Should contain type itself and
@@ -73,6 +83,23 @@ class KType {
    */
   llvm::Type *getRawType() const;
 
+  /**
+   * Getter for the size.
+   */
+  size_t getSize() const;
+
+  /**
+   * Getter for the alignment.
+   */
+  size_t getAlignment() const;
+
+  /**
+   * Return alignment requirements for that object and
+   * it subobjects. If no such restrictions can be applied
+   * returns ref to null expression.
+   */
+  virtual ref<Expr> getContentRestrictions(ref<Expr>) const;
+
   TypeSystemKind getTypeSystemKind() const;
 
   virtual void print(llvm::raw_ostream &) const;
diff --git a/lib/Core/CXXTypeSystem/CXXTypeManager.cpp b/lib/Core/CXXTypeSystem/CXXTypeManager.cpp
index a4488a899e..234ce18844 100644
--- a/lib/Core/CXXTypeSystem/CXXTypeManager.cpp
+++ b/lib/Core/CXXTypeSystem/CXXTypeManager.cpp
@@ -44,7 +44,8 @@ KType *CXXTypeManager::getWrappedType(llvm::Type *type) {
       /* Vector types are considered as their elements type */
       llvm::Type *unwrappedRawType = type;
       if (unwrappedRawType->isVectorTy()) {
-        unwrappedRawType = llvm::cast<llvm::VectorType>(unwrappedRawType)->getElementType();
+        unwrappedRawType =
+            llvm::cast<llvm::VectorType>(unwrappedRawType)->getElementType();
       }
 
       switch (unwrappedRawType->getTypeID()) {
@@ -54,6 +55,10 @@ KType *CXXTypeManager::getWrappedType(llvm::Type *type) {
       case (llvm::Type::IntegerTyID):
         kt = new cxxtypes::KCXXIntegerType(unwrappedRawType, this);
         break;
+      case (llvm::Type::PPC_FP128TyID):
+      case (llvm::Type::FP128TyID):
+      case (llvm::Type::X86_FP80TyID):
+      case (llvm::Type::DoubleTyID):
       case (llvm::Type::FloatTyID):
         kt = new cxxtypes::KCXXFloatingPointType(unwrappedRawType, this);
         break;
@@ -172,6 +177,38 @@ void CXXTypeManager::onFinishInitModule() {
   }
 }
 
+/**
+ * Util method to create constraints for pointers
+ * for complex structures that can have many types located
+ * by different offsets.
+ */
+static ref<Expr> getComplexPointerRestrictions(
+    ref<Expr> object,
+    const std::vector<std::pair<size_t, KType *>> &offsetsToTypes) {
+  ref<Expr> resultCondition;
+  for (auto &offsetToTypePair : offsetsToTypes) {
+    size_t offset = offsetToTypePair.first;
+    KType *extractedType = offsetToTypePair.second;
+
+    ref<Expr> extractedOffset = ExtractExpr::create(
+        object, offset * CHAR_BIT, extractedType->getSize() * CHAR_BIT);
+    ref<Expr> innerAlignmentRequirement =
+        llvm::cast<cxxtypes::KCXXType>(extractedType)
+            ->getPointersRestrictions(extractedOffset);
+    if (innerAlignmentRequirement.isNull()) {
+      continue;
+    }
+
+    if (resultCondition.isNull()) {
+      resultCondition = innerAlignmentRequirement;
+    } else {
+      resultCondition =
+          AndExpr::create(resultCondition, innerAlignmentRequirement);
+    }
+  }
+  return resultCondition;
+}
+
 /* C++ KType base class */
 cxxtypes::KCXXType::KCXXType(llvm::Type *type, TypeManager *parent)
     : KType(type, parent) {
@@ -193,6 +230,19 @@ bool cxxtypes::KCXXType::isAccessableFrom(KType *accessingType) const {
   assert(false && "Attempted to compare raw llvm type with C++ type!");
 }
 
+ref<Expr> cxxtypes::KCXXType::getContentRestrictions(ref<Expr> object) const {
+  if (type == nullptr) {
+    return nullptr;
+  }
+  llvm::Type *elementType = type->getPointerElementType();
+  return llvm::cast<cxxtypes::KCXXType>(parent->getWrappedType(elementType))
+      ->getPointersRestrictions(object);
+}
+
+ref<Expr> cxxtypes::KCXXType::getPointersRestrictions(ref<Expr>) const {
+  return nullptr;
+}
+
 bool cxxtypes::KCXXType::isAccessingFromChar(KCXXType *accessingType) {
   /* Special case for unknown type */
   if (accessingType->getRawType() == nullptr) {
@@ -231,6 +281,19 @@ cxxtypes::KCXXCompositeType::KCXXCompositeType(KType *type, TypeManager *parent,
   insertedTypes.emplace(type);
 }
 
+ref<Expr>
+cxxtypes::KCXXCompositeType::getPointersRestrictions(ref<Expr> object) const {
+  if (containsSymbolic) {
+    return nullptr;
+  }
+  std::vector<std::pair<size_t, KType *>> offsetToTypes;
+  for (auto &offsetToTypePair : typesLocations) {
+    offsetToTypes.emplace_back(offsetToTypePair.first,
+                               offsetToTypePair.second.first);
+  }
+  return getComplexPointerRestrictions(object, offsetToTypes);
+}
+
 void cxxtypes::KCXXCompositeType::handleMemoryAccess(KType *type,
                                                      ref<Expr> offset,
                                                      ref<Expr> size,
@@ -411,6 +474,21 @@ cxxtypes::KCXXStructType::KCXXStructType(llvm::Type *type, TypeManager *parent)
   }
 }
 
+ref<Expr>
+cxxtypes::KCXXStructType::getPointersRestrictions(ref<Expr> object) const {
+  std::vector<std::pair<size_t, KType *>> offsetsToTypes;
+  for (auto &innerTypeToOffsets : innerTypes) {
+    KType *innerType = innerTypeToOffsets.first;
+    if (!llvm::isa<KCXXPointerType>(innerType)) {
+      continue;
+    }
+    for (auto &offset : innerTypeToOffsets.second) {
+      offsetsToTypes.emplace_back(offset, innerType);
+    }
+  }
+  return getComplexPointerRestrictions(object, offsetsToTypes);
+}
+
 bool cxxtypes::KCXXStructType::isAccessableFrom(KCXXType *accessingType) const {
   /* FIXME: this is a temporary hack for vtables in C++. Ideally, we
    * should demangle global variables to get additional info, at least
@@ -460,6 +538,15 @@ cxxtypes::KCXXArrayType::KCXXArrayType(llvm::Type *type, TypeManager *parent)
   arrayElementsCount = rawArrayType->getArrayNumElements();
 }
 
+ref<Expr>
+cxxtypes::KCXXArrayType::getPointersRestrictions(ref<Expr> object) const {
+  std::vector<std::pair<size_t, KType *>> offsetsToTypes;
+  for (unsigned idx = 0; idx < arrayElementsCount; ++idx) {
+    offsetsToTypes.emplace_back(idx * elementType->getSize(), elementType);
+  }
+  return getComplexPointerRestrictions(object, offsetsToTypes);
+}
+
 bool cxxtypes::KCXXArrayType::isAccessableFrom(KCXXType *accessingType) const {
   if (llvm::isa<KCXXArrayType>(accessingType)) {
     return innerIsAccessableFrom(llvm::cast<KCXXArrayType>(accessingType));
@@ -575,6 +662,26 @@ bool cxxtypes::KCXXPointerType::innerIsAccessableFrom(
   return accessingType->getRawType() == nullptr;
 }
 
+ref<Expr>
+cxxtypes::KCXXPointerType::getPointersRestrictions(ref<Expr> object) const {
+  /**
+   * We assume that alignment is always a power of 2 and has
+   * a bit representation as 00...010...00. By subtracting 1
+   * we are getting 00...011...1. Then we apply this mask to
+   * address and require, that bitwise AND should give 0 (i.e.
+   * non of the last bits is 1).
+   */
+  ref<Expr> appliedAlignmentMask = AndExpr::create(
+      Expr::createPointer(elementType->getAlignment() - 1), object);
+
+  ref<Expr> sizeExpr = Expr::createPointer(elementType->getSize() - 1);
+
+  ref<Expr> objectUpperBound = AddExpr::create(object, sizeExpr);
+
+  return AndExpr::create(Expr::createIsZero(appliedAlignmentMask),
+                         UgeExpr::create(objectUpperBound, sizeExpr));
+}
+
 bool cxxtypes::KCXXPointerType::innerIsAccessableFrom(
     KCXXPointerType *accessingType) const {
   return elementType->isAccessableFrom(accessingType->elementType);
diff --git a/lib/Core/CXXTypeSystem/CXXTypeManager.h b/lib/Core/CXXTypeSystem/CXXTypeManager.h
index 33a62d169c..cdc7f42360 100644
--- a/lib/Core/CXXTypeSystem/CXXTypeManager.h
+++ b/lib/Core/CXXTypeSystem/CXXTypeManager.h
@@ -91,6 +91,9 @@ class KCXXType : public KType {
   virtual bool isAccessableFrom(KType *) const final override;
   virtual bool isAccessableFrom(KCXXType *) const;
 
+  virtual ref<Expr> getContentRestrictions(ref<Expr>) const override;
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const;
+
   CXXTypeKind getTypeKind() const;
 
   static bool classof(const KType *);
@@ -115,6 +118,7 @@ class KCXXCompositeType : public KCXXType {
   KCXXCompositeType(KType *, TypeManager *, ref<Expr>);
 
 public:
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const override;
   virtual void handleMemoryAccess(KType *, ref<Expr>, ref<Expr> size,
                                   bool isWrite) override;
   virtual bool isAccessableFrom(KCXXType *) const override;
@@ -137,6 +141,7 @@ class KCXXStructType : public KCXXType {
   KCXXStructType(llvm::Type *, TypeManager *);
 
 public:
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const override;
   virtual bool isAccessableFrom(KCXXType *) const override;
 
   static bool classof(const KType *);
@@ -224,6 +229,7 @@ class KCXXArrayType : public KCXXType {
   KCXXArrayType(llvm::Type *, TypeManager *);
 
 public:
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const override;
   virtual bool isAccessableFrom(KCXXType *) const override;
 
   static bool classof(const KType *);
@@ -245,7 +251,9 @@ class KCXXPointerType : public KCXXType {
   KCXXPointerType(llvm::Type *, TypeManager *);
 
 public:
+  virtual ref<Expr> getPointersRestrictions(ref<Expr>) const override;
   virtual bool isAccessableFrom(KCXXType *) const override;
+
   bool isPointerToChar() const;
   bool isPointerToFunction() const;
 
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index cde70b9a62..6af6690e19 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -159,6 +159,12 @@ cl::opt<bool>
             cl::desc("Turns on restrictions based on types compatibility for "
                      "symbolic pointers (default=false)"),
             cl::init(false));
+
+cl::opt<bool>
+    AlignSymbolicPointers("align-symbolic-pointers",
+                          cl::desc("Makes symbolic pointers aligned according"
+                                   "to the used type system (default=true)"),
+                          cl::init(true));
 } // namespace klee
 
 namespace {
@@ -5002,7 +5008,19 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     if (!unbound)
       break;
   }
-  
+
+
+  if (unbound) {
+    StatePair branches =
+        fork(*unbound, Expr::createIsZero(base), true, BranchType::MemOp);
+    ExecutionState *bound = branches.first;
+    if (bound) {
+      terminateStateOnError(*bound, "memory error: null pointer exception",
+                            StateTerminationType::Ptr);
+    }
+    unbound = branches.second;
+  }
+
   // XXX should we distinguish out of bounds and overlapped cases?
   if (unbound) {
     if (incomplete) {
@@ -5122,7 +5140,15 @@ void Executor::executeMakeSymbolic(ExecutionState &state,
     const Array *array = makeArray(state, mo->size, name);
     const_cast<Array*>(array)->binding = mo;
     const_cast<MemoryObject *>(mo)->isKleeMakeSymbolic = true;
-    bindObjectInState(state, mo, type, isLocal, array);
+    ObjectState *os = bindObjectInState(state, mo, type, isLocal, array);
+
+    if (AlignSymbolicPointers) {
+      if (ref<Expr> alignmentRestrictions =
+              type->getContentRestrictions(os->read(0, os->size * CHAR_BIT))) {
+        addConstraint(state, alignmentRestrictions);
+      }
+    }
+
     state.addSymbolic(mo, array);
     
     std::map< ExecutionState*, std::vector<SeedInfo> >::iterator it = 
diff --git a/lib/Core/TypeManager.cpp b/lib/Core/TypeManager.cpp
index 9ff4d6a5fc..1a7b7cee3b 100644
--- a/lib/Core/TypeManager.cpp
+++ b/lib/Core/TypeManager.cpp
@@ -92,7 +92,7 @@ void TypeManager::initTypesFromStructs() {
     dfs(structType);
   }
 
-  for (auto structType : sortedStructTypesGraph) {  
+  for (auto structType : sortedStructTypesGraph) {
     if (structType->isOpaque()) {
       continue;
     }
@@ -160,6 +160,16 @@ void TypeManager::initTypesFromInstructions() {
   }
 }
 
+void TypeManager::initTypeInfo() {
+  for (auto &type : types) {
+    llvm::Type *rawType = type->getRawType();
+    if (rawType && rawType->isSized()) {
+      type->alignment = parent->targetData->getABITypeAlignment(rawType);
+      type->typeStoreSize = parent->targetData->getTypeStoreSize(rawType);
+    }
+  }
+}
+
 void TypeManager::onFinishInitModule() {}
 
 /**
@@ -174,5 +184,6 @@ void TypeManager::initModule() {
   initTypesFromGlobals();
   initTypesFromInstructions();
   initTypesFromStructs();
+  initTypeInfo();
   onFinishInitModule();
 }
diff --git a/lib/Core/TypeManager.h b/lib/Core/TypeManager.h
index a6bed0bbb9..515f50aafb 100644
--- a/lib/Core/TypeManager.h
+++ b/lib/Core/TypeManager.h
@@ -30,6 +30,7 @@ class TypeManager {
   void initTypesFromGlobals();
   void initTypesFromStructs();
   void initTypesFromInstructions();
+  void initTypeInfo();
 
 protected:
   KModule *parent;
diff --git a/lib/Module/KType.cpp b/lib/Module/KType.cpp
index 1e65d4994e..209de4992d 100644
--- a/lib/Module/KType.cpp
+++ b/lib/Module/KType.cpp
@@ -24,12 +24,16 @@ bool KType::isAccessableFrom(KType *accessingType) const { return true; }
 
 llvm::Type *KType::getRawType() const { return type; }
 
-TypeSystemKind KType::getTypeSystemKind() const {
-  return typeSystemKind;
-}
+TypeSystemKind KType::getTypeSystemKind() const { return typeSystemKind; }
 
 void KType::handleMemoryAccess(KType *, ref<Expr>, ref<Expr>, bool isWrite) {}
 
+size_t KType::getSize() const { return typeStoreSize; }
+
+size_t KType::getAlignment() const { return alignment; }
+
+ref<Expr> KType::getContentRestrictions(ref<Expr>) const { return nullptr; }
+
 void KType::print(llvm::raw_ostream &os) const {
   if (type == nullptr) {
     os << "nullptr";
diff --git a/test/Feature/NullPointerDereferenceCheck.c b/test/Feature/NullPointerDereferenceCheck.c
new file mode 100644
index 0000000000..f06f323955
--- /dev/null
+++ b/test/Feature/NullPointerDereferenceCheck.c
@@ -0,0 +1,12 @@
+// RUN: %clang %s -emit-llvm -g -c -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --use-gep-expr %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+
+int main() {
+  int *ptr;
+  klee_make_symbolic(&ptr, sizeof(ptr), "ptr");
+  // CHECK: NullPointerDereferenceCheck.c:[[@LINE+1]]: memory error: null pointer exception
+  *ptr = 10;
+}
diff --git a/test/Feature/types/ArrayAccess.c b/test/Feature/types/ArrayAccess.c
index e68749b4ec..861518eade 100644
--- a/test/Feature/types/ArrayAccess.c
+++ b/test/Feature/types/ArrayAccess.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
@@ -17,7 +17,7 @@ int main() {
   // CHECK-NOT: ASSERTION FAIL
   assert((void *)ptr != (void *)array_float);
 
-  // CHECK: x
+  // CHECK-DAG: x
   if ((void *)ptr == (void *)array_int) {
     printf("x\n");
     return 0;
@@ -30,7 +30,7 @@ int main() {
   // CHECK-NOT: ASSERTION FAIL
   assert((void *)ptr_array_float != (void *)&array_int);
 
-  // CHECK: y
+  // CHECK-DAG: y
   if (ptr_array_float == &array_float) {
     printf("y\n");
     return 2;
diff --git a/test/Feature/types/InnerStructAccess.c b/test/Feature/types/InnerStructAccess.c
index 7eb8dc6930..9c7008faf2 100644
--- a/test/Feature/types/InnerStructAccess.c
+++ b/test/Feature/types/InnerStructAccess.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
diff --git a/test/Feature/types/StructDereference.c b/test/Feature/types/StructDereference.c
index 840e74b3ac..db643ca9ae 100644
--- a/test/Feature/types/StructDereference.c
+++ b/test/Feature/types/StructDereference.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
diff --git a/test/Feature/types/SymbolicPointerMultipleResolve.c b/test/Feature/types/SymbolicPointerMultipleResolve.c
index a473b1b44e..a438f92d10 100644
--- a/test/Feature/types/SymbolicPointerMultipleResolve.c
+++ b/test/Feature/types/SymbolicPointerMultipleResolve.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
@@ -45,10 +45,10 @@ int main() {
   char *anyPointer;
   klee_make_symbolic(&anyPointer, sizeof(anyPointer), "anyPointer");
   *anyPointer = '0';
-  // CHECK: a
-  // CHECK: b
-  // CHECK: c
-  // CHECK: d
+  // CHECK-DAG: a
+  // CHECK-DAG: b
+  // CHECK-DAG: c
+  // CHECK-DAG: d
   if ((void *)anyPointer == (void *)&a) {
     printf("a\n");
     return 0;
diff --git a/test/Feature/types/UnionAccess.c b/test/Feature/types/UnionAccess.c
index b22ca4196d..828402e594 100644
--- a/test/Feature/types/UnionAccess.c
+++ b/test/Feature/types/UnionAccess.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
diff --git a/test/Feature/types/effective-type/EffectiveTypeFirstRead.c b/test/Feature/types/effective-type/EffectiveTypeFirstRead.c
index 463379eccc..a9b8936bff 100644
--- a/test/Feature/types/effective-type/EffectiveTypeFirstRead.c
+++ b/test/Feature/types/effective-type/EffectiveTypeFirstRead.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
@@ -19,11 +19,11 @@ int main() {
   klee_make_symbolic(&pointer, sizeof(pointer), "pointer");
   *pointer = 1;
 
-  // CHECK: x
+  // CHECK-DAG: x
   if ((void *)pointer == (void *)area) {
     printf("x\n");
     // CHECK-NOT: ASSERTION FAIL
-    assert(area[3] == 1);
+    assert((area[0] == 1) ^ (area[3] == 1));
   }
 
   return 0;
diff --git a/test/Feature/types/effective-type/EffectiveTypeMalloc.c b/test/Feature/types/effective-type/EffectiveTypeMalloc.c
index bd80e2a4eb..53b05d08ab 100644
--- a/test/Feature/types/effective-type/EffectiveTypeMalloc.c
+++ b/test/Feature/types/effective-type/EffectiveTypeMalloc.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
diff --git a/test/Feature/types/effective-type/EffectiveTypeMemset.c b/test/Feature/types/effective-type/EffectiveTypeMemset.c
index a46ef0d7ed..cb7cfa8c34 100644
--- a/test/Feature/types/effective-type/EffectiveTypeMemset.c
+++ b/test/Feature/types/effective-type/EffectiveTypeMemset.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 
@@ -20,7 +20,7 @@ int main() {
 
   int created = 0;
 
-  // CHECK: x
+  // CHECK-DAG: x
   if ((void *)float_ptr == (void *)area) {
     ++created;
     printf("x\n");
@@ -30,8 +30,8 @@ int main() {
   klee_make_symbolic(&int_ptr, sizeof(int_ptr), "int_ptr");
   *int_ptr = 11;
 
-  // CHECK: y
-  // CHECK: z
+  // CHECK-DAG: y
+  // CHECK-DAG: z
   if ((void *)int_ptr == (void *)area + sizeof(float)) {
     ++created;
     printf(created == 2 ? "z\n" : "y\n");
diff --git a/test/Feature/types/effective-type/EffectiveTypeRealloc.c b/test/Feature/types/effective-type/EffectiveTypeRealloc.c
index a5c1c1d59e..df5910318a 100644
--- a/test/Feature/types/effective-type/EffectiveTypeRealloc.c
+++ b/test/Feature/types/effective-type/EffectiveTypeRealloc.c
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc | FileCheck %s
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <assert.h>
@@ -25,7 +25,7 @@ int main() {
   klee_make_symbolic(&ptr_int, sizeof(ptr_int), "ptr_int");
   *ptr_int = 100;
 
-  // CHECK: x
+  // CHECK-DAG: x
   if ((void *)ptr_int == area) {
     printf("x\n");
     return 0;
@@ -34,7 +34,7 @@ int main() {
   float *ptr_float;
   klee_make_symbolic(&ptr_float, sizeof(ptr_float), "ptr_float");
   *ptr_float = 100.0;
-  // CHECK: y
+  // CHECK-DAG: y
   if ((void *)ptr_float >= area + 4) {
     printf("y\n");
     return 0;
diff --git a/test/Feature/types/effective-type/OperatorNew.cpp b/test/Feature/types/effective-type/OperatorNew.cpp
index 1fe5a1300e..832c4bdf41 100644
--- a/test/Feature/types/effective-type/OperatorNew.cpp
+++ b/test/Feature/types/effective-type/OperatorNew.cpp
@@ -1,6 +1,6 @@
 // RUN: %clang %s -emit-llvm -g -c -o %t.bc
 // RUN: rm -rf %t.klee-out
-// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --use-gep-expr %t.bc 2>&1 | FileCheck %s
 
 #include "klee/klee.h"
 #include <cassert>
@@ -26,7 +26,7 @@ int main() {
   klee_make_symbolic(&ptr_int, sizeof(ptr_int), "ptr_int");
   *ptr_int = 100;
 
-  // CHECK: x
+  // CHECK-DAG: x
   if (isSameAddress(ptr_int, s)) {
     printf("x\n");
     return 0;
@@ -36,7 +36,7 @@ int main() {
   klee_make_symbolic(&ptr_float, sizeof(ptr_float), "ptr_float");
   *ptr_float = 10.f;
 
-  // CHECK: y
+  // CHECK-DAG: y
   if (isSameAddress(ptr_float, s)) {
     printf("y\n");
     return 0;
diff --git a/test/Feature/types/pointers-alignment/ArrayPointerAlignment.c b/test/Feature/types/pointers-alignment/ArrayPointerAlignment.c
new file mode 100644
index 0000000000..e13af669a4
--- /dev/null
+++ b/test/Feature/types/pointers-alignment/ArrayPointerAlignment.c
@@ -0,0 +1,23 @@
+// RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --align-symbolic-pointers=true --use-gep-expr %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+int main() {
+  int16_t value = 0;
+
+  int16_t *array[2];
+  klee_make_symbolic(&array, sizeof(array), "array");
+
+  // CHECK: x
+  if (!array[1]) {
+    printf("x");
+    return 0;
+  }
+
+  // CHECK-NOT: ArrayPointerAlignment.c:[[@LINE+1]]: either misaligned address 0x{{.*}} or invalid usage of address 0x{{.*}} with insufficient space
+  *(array[1]) = 100;
+  return 0;
+}
diff --git a/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c b/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c
new file mode 100644
index 0000000000..c0f468803a
--- /dev/null
+++ b/test/Feature/types/pointers-alignment/DefaultPointerAlignment.c
@@ -0,0 +1,24 @@
+// RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --align-symbolic-pointers=true --use-gep-expr %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+int main() {
+  float value;
+
+  float *ptr;
+  klee_make_symbolic(&ptr, sizeof(ptr), "ptr");
+
+  // CHECK-NOT: DefaultPointerAlignment.c:[[@LINE+1]]: either misaligned address for 0x{{.*}} or invalid usage of address 0x{{.*}} with insufficient space
+  *ptr = 10;
+
+  int n = klee_range(1, 4, "n");
+  ptr = (float *)(((char *)ptr) + n);
+
+  // CHECK: DefaultPointerAlignment.c:[[@LINE+1]]: either misaligned address for 0x{{.*}} or invalid usage of address 0x{{.*}} with insufficient space
+  *ptr = 20;
+
+  return 0;
+}
diff --git a/test/Feature/types/pointers-alignment/EffectiveTypePointerAlignment.c b/test/Feature/types/pointers-alignment/EffectiveTypePointerAlignment.c
new file mode 100644
index 0000000000..4721f48f5a
--- /dev/null
+++ b/test/Feature/types/pointers-alignment/EffectiveTypePointerAlignment.c
@@ -0,0 +1,26 @@
+// RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=false --align-symbolic-pointers=true --use-gep-expr %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdlib.h>
+
+int main() {
+  int outer_int_value;
+  double outer_float_value;
+
+  void *area = malloc(sizeof(int *) + sizeof(double *));
+
+  int **int_place = area;
+  double **double_place = area + sizeof(int *);
+
+  *int_place = 0;
+  *double_place = 0;
+
+  klee_make_symbolic(area, sizeof(int *) + sizeof(double *), "area");
+
+  // CHECK-NOT: EffectiveTypePointerAlignment.c:[[@LINE+1]]: either misaligned address for 0x{{.*}} or invalid usage of address 0x{{.*}} with insufficient space
+  **int_place = 10;
+  // CHECK-NOT: EffectiveTypePointerAlignment.c:[[@LINE+1]]: either misaligned address for 0x{{.*}} or invalid usage of address 0x{{.*}} with insufficient space
+  **double_place = 20;
+}
diff --git a/test/Feature/types/pointers-alignment/StructurePointerAlignment.c b/test/Feature/types/pointers-alignment/StructurePointerAlignment.c
new file mode 100644
index 0000000000..eabc8beac2
--- /dev/null
+++ b/test/Feature/types/pointers-alignment/StructurePointerAlignment.c
@@ -0,0 +1,31 @@
+// RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=true --align-symbolic-pointers=true --use-gep-expr %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+struct Node {
+  struct Node *next;
+  int x;
+};
+
+void foo(struct Node *head) {
+  if (head->next) {
+    // CHECK-DAG: x
+    printf("x\n");
+    // CHECK-NOT: StructurePointerAlignment.c:[[@LINE+1]]: either misaligned address for 0x{{.*}} or invalid usage of address 0x{{.*}} with insufficient space
+    head->next->x = 100;
+  } else {
+    // CHECK-DAG: y
+    printf("y\n");
+  }
+}
+
+int main() {
+  struct Node head;
+  klee_make_symbolic(&head, sizeof(head), "head");
+  klee_prefer_cex(&head, head.x >= -10 & head.x <= 10);
+  foo(&head);
+  return 0;
+}
diff --git a/test/Feature/types/pointers-alignment/StructurePointerWithOffsetAlignment.c b/test/Feature/types/pointers-alignment/StructurePointerWithOffsetAlignment.c
new file mode 100644
index 0000000000..dec37cba4a
--- /dev/null
+++ b/test/Feature/types/pointers-alignment/StructurePointerWithOffsetAlignment.c
@@ -0,0 +1,35 @@
+// RUN: %clang %s -emit-llvm -g -c -fsanitize=alignment,null -o %t.bc
+// RUN: rm -rf %t.klee-out
+// RUN: %klee --output-dir=%t.klee-out --type-system=CXX --use-tbaa --lazy-instantiation=true --align-symbolic-pointers=true --use-gep-expr %t.bc 2>&1 | FileCheck %s
+
+#include "klee/klee.h"
+#include <stdio.h>
+
+struct Node {
+  struct Node *next;
+  int x;
+};
+
+void foo(struct Node *head, int n) {
+  char *pointer = head->next;
+  pointer += n;
+  head = (struct Node *)pointer;
+
+  if ((n & (sizeof(int) - 1)) == 0) {
+    // CHECK-DAG: x
+    printf("x\n");
+    // CHECK-NOT: StructurePointerWithOffsetAlignment.c:[[@LINE+1]]: either misaligned address for 0x{{.*}} or invalid usage of address 0x{{.*}} with insufficient space
+    head->x = 100;
+  } else {
+    // CHECK: StructurePointerWithOffsetAlignment.c:[[@LINE+1]]: either misaligned address for 0x{{.*}} or invalid usage of address 0x{{.*}} with insufficient space
+    head->x = 100;
+  }
+}
+
+int main() {
+  struct Node head;
+  klee_make_symbolic(&head, sizeof(head), "head");
+  int n = klee_range(0, 4, "n");
+  foo(&head, n);
+  return 0;
+}