diff --git a/CMakeLists.txt b/CMakeLists.txt
index 40f5078cc..ed84b3460 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -179,6 +179,7 @@ add_library(smackTranslator STATIC
   include/smack/IntegerOverflowChecker.h
   include/smack/NormalizeLoops.h
   include/smack/SplitAggregateValue.h
+  include/smack/ModAnalysis.h
   include/smack/Prelude.h
   include/smack/SmackWarnings.h
   lib/smack/AddTiming.cpp
@@ -203,6 +204,7 @@ add_library(smackTranslator STATIC
   lib/smack/IntegerOverflowChecker.cpp
   lib/smack/NormalizeLoops.cpp
   lib/smack/SplitAggregateValue.cpp
+  lib/smack/ModAnalysis.cpp
   lib/smack/Prelude.cpp
   lib/smack/SmackWarnings.cpp
 )
diff --git a/include/smack/BoogieAst.h b/include/smack/BoogieAst.h
index ffddfeac0..a62e984c2 100644
--- a/include/smack/BoogieAst.h
+++ b/include/smack/BoogieAst.h
@@ -16,6 +16,37 @@ enum class RModeKind { RNE, RNA, RTP, RTN, RTZ };
 
 class Expr {
 public:
+  enum Kind {
+    BIN,
+    COND,
+    FUN,
+    BOOL_LIT,
+    RMODE_LIT,
+    INT_LIT,
+    BV_LIT,
+    FP_LIT,
+    STRING_LIT,
+    NEG,
+    NOT,
+    QUANT,
+    SEL,
+    UPD,
+    VAR,
+    IF_THEN_ELSE,
+    BV_EXTRACT,
+    BV_CONCAT,
+    CODE
+  };
+
+private:
+  const Kind kind;
+
+protected:
+  Expr(Kind k) : kind(k) {}
+
+public:
+  Kind getKind() const { return kind; }
+
   virtual ~Expr() {}
   virtual void print(std::ostream &os) const = 0;
   static const Expr *exists(std::list<Binding>, const Expr *e);
@@ -84,8 +115,9 @@ class BinExpr : public Expr {
 
 public:
   BinExpr(const Binary b, const Expr *l, const Expr *r)
-      : op(b), lhs(l), rhs(r) {}
+      : Expr(BIN), op(b), lhs(l), rhs(r) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == BIN; }
 };
 
 class FunExpr : public Expr {
@@ -93,42 +125,48 @@ class FunExpr : public Expr {
   std::list<const Expr *> args;
 
 public:
-  FunExpr(std::string f, std::list<const Expr *> xs) : fun(f), args(xs) {}
+  FunExpr(std::string f, std::list<const Expr *> xs)
+      : Expr(FUN), fun(f), args(xs) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == FUN; }
+  std::list<const Expr *> getArgs() const { return args; }
 };
 
 class BoolLit : public Expr {
   bool val;
 
 public:
-  BoolLit(bool b) : val(b) {}
+  BoolLit(bool b) : Expr(BOOL_LIT), val(b) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == BOOL_LIT; }
 };
 
 class RModeLit : public Expr {
   RModeKind val;
 
 public:
-  RModeLit(RModeKind v) : val(v) {}
+  RModeLit(RModeKind v) : Expr(RMODE_LIT), val(v) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == RMODE_LIT; }
 };
 
 class IntLit : public Expr {
   std::string val;
 
 public:
-  IntLit(std::string v) : val(v) {}
-  IntLit(unsigned long long v) {
+  IntLit(std::string v) : Expr(INT_LIT), val(v) {}
+  IntLit(unsigned long long v) : Expr(INT_LIT) {
     std::stringstream s;
     s << v;
     val = s.str();
   }
-  IntLit(long long v) {
+  IntLit(long long v) : Expr(INT_LIT) {
     std::stringstream s;
     s << v;
     val = s.str();
   }
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == INT_LIT; }
 };
 
 class BvLit : public Expr {
@@ -136,13 +174,14 @@ class BvLit : public Expr {
   unsigned width;
 
 public:
-  BvLit(std::string v, unsigned w) : val(v), width(w) {}
-  BvLit(unsigned long long v, unsigned w) : width(w) {
+  BvLit(std::string v, unsigned w) : Expr(BV_LIT), val(v), width(w) {}
+  BvLit(unsigned long long v, unsigned w) : Expr(BV_LIT), width(w) {
     std::stringstream s;
     s << v;
     val = s.str();
   }
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == BV_LIT; }
 };
 
 class FPLit : public Expr {
@@ -155,34 +194,38 @@ class FPLit : public Expr {
 
 public:
   FPLit(bool n, std::string s, std::string e, unsigned ss, unsigned es)
-      : neg(n), sig(s), expo(e), sigSize(ss), expSize(es) {}
+      : Expr(FP_LIT), neg(n), sig(s), expo(e), sigSize(ss), expSize(es) {}
   FPLit(std::string v, unsigned ss, unsigned es)
-      : specialValue(v), sigSize(ss), expSize(es) {}
+      : Expr(FP_LIT), specialValue(v), sigSize(ss), expSize(es) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == FP_LIT; }
 };
 
 class StringLit : public Expr {
   std::string val;
 
 public:
-  StringLit(std::string v) : val(v) {}
+  StringLit(std::string v) : Expr(STRING_LIT), val(v) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == STRING_LIT; }
 };
 
 class NegExpr : public Expr {
   const Expr *expr;
 
 public:
-  NegExpr(const Expr *e) : expr(e) {}
+  NegExpr(const Expr *e) : Expr(NEG), expr(e) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == NEG; }
 };
 
 class NotExpr : public Expr {
   const Expr *expr;
 
 public:
-  NotExpr(const Expr *e) : expr(e) {}
+  NotExpr(const Expr *e) : Expr(NOT), expr(e) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == NOT; }
 };
 
 class QuantExpr : public Expr {
@@ -196,8 +239,9 @@ class QuantExpr : public Expr {
 
 public:
   QuantExpr(Quantifier q, std::list<Binding> vs, const Expr *e)
-      : quant(q), vars(vs), expr(e) {}
+      : Expr(QUANT), quant(q), vars(vs), expr(e) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == QUANT; }
 };
 
 class SelExpr : public Expr {
@@ -205,10 +249,12 @@ class SelExpr : public Expr {
   std::list<const Expr *> idxs;
 
 public:
-  SelExpr(const Expr *a, std::list<const Expr *> i) : base(a), idxs(i) {}
+  SelExpr(const Expr *a, std::list<const Expr *> i)
+      : Expr(SEL), base(a), idxs(i) {}
   SelExpr(const Expr *a, const Expr *i)
-      : base(a), idxs(std::list<const Expr *>(1, i)) {}
+      : Expr(SEL), base(a), idxs(std::list<const Expr *>(1, i)) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == SEL; }
 };
 
 class UpdExpr : public Expr {
@@ -218,19 +264,21 @@ class UpdExpr : public Expr {
 
 public:
   UpdExpr(const Expr *a, std::list<const Expr *> i, const Expr *v)
-      : base(a), idxs(i), val(v) {}
+      : Expr(UPD), base(a), idxs(i), val(v) {}
   UpdExpr(const Expr *a, const Expr *i, const Expr *v)
-      : base(a), idxs(std::list<const Expr *>(1, i)), val(v) {}
+      : Expr(UPD), base(a), idxs(std::list<const Expr *>(1, i)), val(v) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == UPD; }
 };
 
 class VarExpr : public Expr {
   std::string var;
 
 public:
-  VarExpr(std::string v) : var(v) {}
+  VarExpr(std::string v) : Expr(VAR), var(v) {}
   std::string name() const { return var; }
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == VAR; }
 };
 
 class IfThenElseExpr : public Expr {
@@ -240,8 +288,9 @@ class IfThenElseExpr : public Expr {
 
 public:
   IfThenElseExpr(const Expr *c, const Expr *t, const Expr *e)
-      : cond(c), trueValue(t), falseValue(e) {}
+      : Expr(IF_THEN_ELSE), cond(c), trueValue(t), falseValue(e) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == IF_THEN_ELSE; }
 };
 
 class BvExtract : public Expr {
@@ -251,8 +300,9 @@ class BvExtract : public Expr {
 
 public:
   BvExtract(const Expr *var, const Expr *upper, const Expr *lower)
-      : var(var), upper(upper), lower(lower) {}
+      : Expr(BV_EXTRACT), var(var), upper(upper), lower(lower) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == BV_EXTRACT; }
 };
 
 class BvConcat : public Expr {
@@ -260,8 +310,10 @@ class BvConcat : public Expr {
   const Expr *right;
 
 public:
-  BvConcat(const Expr *left, const Expr *right) : left(left), right(right) {}
+  BvConcat(const Expr *left, const Expr *right)
+      : Expr(BV_CONCAT), left(left), right(right) {}
   void print(std::ostream &os) const;
+  static bool classof(const Expr *e) { return e->getKind() == BV_CONCAT; }
 };
 
 class Attr {
@@ -354,6 +406,8 @@ class AssignStmt : public Stmt {
 public:
   AssignStmt(std::list<const Expr *> lhs, std::list<const Expr *> rhs)
       : Stmt(ASSIGN), lhs(lhs), rhs(rhs) {}
+  std::list<const Expr *> getlhs() const { return lhs; }
+  std::list<const Expr *> getrhs() const { return rhs; }
   void print(std::ostream &os) const;
   static bool classof(const Stmt *S) { return S->getKind() == ASSIGN; }
 };
@@ -387,6 +441,10 @@ class CallStmt : public Stmt {
            std::list<const Expr *> args, std::list<std::string> rets)
       : Stmt(CALL), proc(p), attrs(attrs), params(args), returns(rets) {}
 
+  std::string getName() const { return proc; }
+  std::list<const Attr *> getAttrs() const { return attrs; }
+  std::list<const Expr *> getParams() const { return params; }
+  std::list<std::string> getReturns() const { return returns; }
   void print(std::ostream &os) const;
   static bool classof(const Stmt *S) { return S->getKind() == CALL; }
 };
@@ -594,8 +652,10 @@ class CodeContainer {
 
 class CodeExpr : public Expr, public CodeContainer {
 public:
-  CodeExpr(DeclarationList ds, BlockList bs) : CodeContainer(ds, bs) {}
+  CodeExpr(DeclarationList ds, BlockList bs)
+      : Expr(CODE), CodeContainer(ds, bs) {}
   void print(std::ostream &os) const;
+  static bool classof(Expr *e) { return e->getKind() == CODE; }
 };
 
 class ProcDecl : public Decl, public CodeContainer {
@@ -661,6 +721,7 @@ class Program {
   bool empty() { return decls.empty(); }
   DeclarationList &getDeclarations() { return decls; }
   void appendPrelude(std::string s) { prelude += s; }
+  std::string &getPrelude() { return prelude; }
 };
 
 std::ostream &operator<<(std::ostream &os, const Expr &e);
diff --git a/include/smack/ModAnalysis.h b/include/smack/ModAnalysis.h
new file mode 100644
index 000000000..9a62942b0
--- /dev/null
+++ b/include/smack/ModAnalysis.h
@@ -0,0 +1,76 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#ifndef MODANALYSIS_H
+#define MODANALYSIS_H
+
+#include "smack/BoogieAst.h"
+#include "smack/SmackModuleGenerator.h"
+#include "llvm/Support/Regex.h"
+#include <map>
+#include <set>
+#include <stack>
+
+namespace smack {
+
+using llvm::Regex;
+
+class ModAnalysis : public llvm::ModulePass {
+
+private:
+  std::stack<std::string> st;
+  std::map<std::string, bool> onStack;
+  std::map<std::string, int> index;
+  std::map<std::string, int> low;
+  std::map<std::string, int> SCCOfProc;
+  std::map<std::string, ProcDecl *> proc;
+  std::vector<std::set<int>> SCCGraph;
+  std::vector<std::set<std::string>> modVars;
+
+  int maxIndex;
+
+  void initProcMap(Program *program);
+  std::string
+  getBplGlobalsModifiesClause(const std::set<std::string> &bplGlobals);
+  void fixPrelude(Program *program, const std::string &modClause);
+  void addModifiesToSmackProcs(Program *program, const std::string &modClause);
+  void genSmackCodeModifies(Program *program,
+                            const std::set<std::string> &bplGlobals);
+  void addNewSCC(const std::string &procName);
+  void dfs(ProcDecl *curProc);
+  void genSCCs(Program *program);
+  void genSCCGraph(Program *program);
+  void addEdge(const CallStmt *callStmt, int parentSCC);
+  void addIfGlobalVar(std::string exprName, const std::string &procName);
+  void calcModifiesOfExprs(const std::list<const Expr *> exprs,
+                           const std::string &procName);
+  void calcModifiesOfStmt(const Stmt *stmt, const std::string procName);
+  void calcModifiesOfSCCs(Program *program);
+  void propagateModifiesUpGraph();
+  void addSmackGlobals(const std::set<std::string> &bplGlobals);
+  void addModifies(Program *program);
+  void genUserCodeModifies(Program *program,
+                           const std::set<std::string> &bplGlobals);
+
+public:
+  static char ID; // Pass identification, replacement for typeid
+
+  ModAnalysis() : llvm::ModulePass(ID), maxIndex(1) {
+    SCCGraph.push_back(std::set<int>());
+    modVars.push_back(std::set<std::string>());
+  }
+
+  virtual bool runOnModule(llvm::Module &m);
+
+  virtual llvm::StringRef getPassName() const {
+    return "Modifies clause generation";
+  }
+
+  virtual void getAnalysisUsage(llvm::AnalysisUsage &AU) const {
+    AU.setPreservesAll();
+    AU.addRequired<SmackModuleGenerator>();
+  }
+};
+}
+
+#endif // MODANALYSIS_H
diff --git a/include/smack/SmackModuleGenerator.h b/include/smack/SmackModuleGenerator.h
index dcfb4df07..7b848fe8f 100644
--- a/include/smack/SmackModuleGenerator.h
+++ b/include/smack/SmackModuleGenerator.h
@@ -13,6 +13,7 @@ class Program;
 class SmackModuleGenerator : public llvm::ModulePass {
 private:
   Program *program;
+  std::vector<std::string> bplGlobals;
 
 public:
   static char ID; // Pass identification, replacement for typeid
@@ -22,6 +23,7 @@ class SmackModuleGenerator : public llvm::ModulePass {
   virtual bool runOnModule(llvm::Module &m);
   void generateProgram(llvm::Module &m);
   Program *getProgram() { return program; }
+  std::vector<std::string> getBplGlobals() { return bplGlobals; }
 };
 } // namespace smack
 
diff --git a/include/smack/SmackRep.h b/include/smack/SmackRep.h
index 2604150e4..4f104c102 100644
--- a/include/smack/SmackRep.h
+++ b/include/smack/SmackRep.h
@@ -188,6 +188,7 @@ class SmackRep {
   void addInitFunc(const llvm::Function *f);
   Decl *getInitFuncs();
   const Expr *declareIsExternal(const Expr *e);
+  std::vector<std::string> getBplGlobals() { return bplGlobals; }
 
   bool isContractExpr(const llvm::Value *V) const;
   bool isContractExpr(const std::string S) const;
diff --git a/lib/smack/ModAnalysis.cpp b/lib/smack/ModAnalysis.cpp
new file mode 100644
index 000000000..4645d76e4
--- /dev/null
+++ b/lib/smack/ModAnalysis.cpp
@@ -0,0 +1,263 @@
+//
+// This file is distributed under the MIT License. See LICENSE for details.
+//
+#include "smack/ModAnalysis.h"
+#include "llvm/Support/Debug.h"
+#include "llvm/Support/GraphWriter.h"
+#include <algorithm>
+#include <iterator>
+#include <list>
+
+namespace smack {
+
+using llvm::errs;
+using llvm::dyn_cast;
+using llvm::isa;
+
+char ModAnalysis::ID = 0;
+
+void ModAnalysis::initProcMap(Program *program) {
+  for (Decl *decl : *program) {
+    if (ProcDecl *procDecl = dyn_cast<ProcDecl>(decl)) {
+      proc[procDecl->getName()] = procDecl;
+    }
+  }
+}
+
+std::string ModAnalysis::getBplGlobalsModifiesClause(
+    const std::set<std::string> &bplGlobals) {
+  std::string modClause = "\nmodifies";
+
+  for (std::string var : bplGlobals) {
+    modClause += " " + var + ",";
+  }
+
+  modClause[modClause.size() - 1] = ';';
+  modClause.push_back('\n');
+
+  return modClause;
+}
+
+void ModAnalysis::fixPrelude(Program *program, const std::string &modClause) {
+  std::string searchStr = "procedure $global_allocations()\n";
+  std::string &prelude = program->getPrelude();
+  size_t pos = prelude.find(searchStr);
+
+  if (pos != std::string::npos) {
+    std::string str1 = prelude.substr(0, pos + searchStr.size());
+    std::string str2 = prelude.substr(pos + searchStr.size());
+    prelude = str1 + modClause + str2;
+  }
+}
+
+void ModAnalysis::addModifiesToSmackProcs(Program *program,
+                                          const std::string &modClause) {
+  const std::string NAME_REGEX = "[[:alpha:]_.$#'`^\?][[:alnum:]_.$#'`^\?]*";
+  Regex PROC_DECL("^([[:space:]]*procedure[[:space:]]+[^\\(]*(" + NAME_REGEX +
+                  ")[[:space:]]*\\([^\\)]*\\)[^\\{]*)(\\{(.|[[:space:]])*(\\}[["
+                  ":space:]]*)$)");
+  Regex MOD_CL("modifies[[:space:]]+" + NAME_REGEX +
+               "([[:space:]]*,[[:space:]]*" + NAME_REGEX + ")*;");
+
+  for (Decl *&decl : *program) {
+    if (isa<CodeDecl>(decl)) {
+      if (PROC_DECL.match(decl->getName()) && !MOD_CL.match(decl->getName())) {
+        std::string newStr = PROC_DECL.sub("\\1", decl->getName()) + modClause +
+                             PROC_DECL.sub("\\3", decl->getName());
+        decl = Decl::code(newStr, newStr);
+      }
+    }
+  }
+}
+
+void ModAnalysis::genSmackCodeModifies(
+    Program *program, const std::set<std::string> &bplGlobals) {
+  std::string modClause = getBplGlobalsModifiesClause(bplGlobals);
+  fixPrelude(program, modClause);
+  addModifiesToSmackProcs(program, modClause);
+}
+
+void ModAnalysis::addNewSCC(const std::string &procName) {
+  std::string toAdd;
+
+  do {
+    toAdd = st.top();
+    st.pop();
+    onStack[toAdd] = false;
+    SCCOfProc[toAdd] = modVars.size();
+  } while (toAdd != procName);
+
+  modVars.push_back(std::set<std::string>());
+  SCCGraph.push_back(std::set<int>());
+}
+
+void ModAnalysis::dfs(ProcDecl *procDecl) {
+  const std::string name = procDecl->getName();
+
+  st.push(name);
+  onStack[name] = true;
+  index[name] = maxIndex;
+  low[name] = maxIndex++;
+
+  for (Block *block : *procDecl) {
+    for (const Stmt *stmt : *block) {
+      if (const CallStmt *callStmt = dyn_cast<CallStmt>(stmt)) {
+        const std::string next = callStmt->getName();
+
+        if (proc.count(next) && !index[next]) {
+          dfs(proc[next]);
+          low[name] = std::min(low[name], low[next]);
+        } else if (onStack[next]) {
+          low[name] = std::min(low[name], index[next]);
+        }
+      }
+    }
+  }
+
+  if (low[name] == index[name]) {
+    addNewSCC(name);
+  }
+}
+
+void ModAnalysis::genSCCs(Program *program) {
+  for (Decl *decl : *program) {
+    if (ProcDecl *procDecl = dyn_cast<ProcDecl>(decl)) {
+      if (!index[procDecl->getName()]) {
+        dfs(procDecl);
+      }
+    }
+  }
+}
+
+void ModAnalysis::addEdge(const CallStmt *callStmt, int parentSCC) {
+  int childSCC = SCCOfProc[callStmt->getName()];
+
+  if (childSCC && childSCC != parentSCC) {
+    SCCGraph[childSCC].insert(parentSCC);
+  }
+}
+
+void ModAnalysis::genSCCGraph(Program *program) {
+  for (Decl *decl : *program) {
+    if (ProcDecl *procDecl = dyn_cast<ProcDecl>(decl)) {
+      int curSCC = SCCOfProc[procDecl->getName()];
+
+      for (Block *block : *procDecl) {
+        for (const Stmt *stmt : *block) {
+          if (const CallStmt *callStmt = dyn_cast<CallStmt>(stmt)) {
+            addEdge(callStmt, curSCC);
+          }
+        }
+      }
+    }
+  }
+}
+
+void ModAnalysis::addIfGlobalVar(const std::string exprName,
+                                 const std::string &procName) {
+  static Regex GLOBAL_VAR("\\$M.[[:digit:]]+");
+  if (GLOBAL_VAR.match(exprName)) {
+    std::string var = GLOBAL_VAR.sub("\\0", exprName);
+
+    modVars[SCCOfProc[procName]].insert(var);
+  }
+}
+
+void ModAnalysis::calcModifiesOfExprs(const std::list<const Expr *> exprs,
+                                      const std::string &procName) {
+  for (auto expr : exprs) {
+    if (const VarExpr *varExpr = dyn_cast<VarExpr>(expr)) {
+      addIfGlobalVar(varExpr->name(), procName);
+    }
+  }
+}
+
+void ModAnalysis::calcModifiesOfStmt(const Stmt *stmt,
+                                     const std::string procName) {
+  if (const AssignStmt *assignStmt = dyn_cast<AssignStmt>(stmt)) {
+    calcModifiesOfExprs(assignStmt->getlhs(), procName);
+
+    for (const Expr *expr : assignStmt->getrhs()) {
+      if (const FunExpr *funExpr = dyn_cast<FunExpr>(expr)) {
+        calcModifiesOfExprs(funExpr->getArgs(), procName);
+      }
+    }
+  } else if (const CallStmt *callStmt = dyn_cast<CallStmt>(stmt)) {
+    for (const std::string retName : callStmt->getReturns()) {
+      addIfGlobalVar(retName, procName);
+    }
+
+    calcModifiesOfExprs(callStmt->getParams(), procName);
+  }
+}
+
+void ModAnalysis::calcModifiesOfSCCs(Program *program) {
+  for (Decl *decl : *program) {
+    if (ProcDecl *procDecl = dyn_cast<ProcDecl>(decl)) {
+      for (Block *block : *procDecl) {
+        for (const Stmt *stmt : *block) {
+          calcModifiesOfStmt(stmt, procDecl->getName());
+        }
+      }
+    }
+  }
+}
+
+void ModAnalysis::propagateModifiesUpGraph() {
+  for (size_t child = 1; child < SCCGraph.size(); ++child) {
+    for (int parent : SCCGraph[child]) {
+      modVars[parent].insert(modVars[child].begin(), modVars[child].end());
+    }
+  }
+}
+
+void ModAnalysis::addSmackGlobals(const std::set<std::string> &bplGlobals) {
+  for (size_t scc = 0; scc < modVars.size(); ++scc) {
+    modVars[scc].insert(bplGlobals.begin(), bplGlobals.end());
+  }
+}
+
+void ModAnalysis::addModifies(Program *program) {
+  for (Decl *decl : *program) {
+    if (ProcDecl *procDecl = dyn_cast<ProcDecl>(decl)) {
+      if (procDecl->begin() != procDecl->end()) {
+        int index = SCCOfProc[procDecl->getName()];
+        std::list<std::string> &modList = procDecl->getModifies();
+        modList.insert(modList.end(), modVars[index].begin(),
+                       modVars[index].end());
+      }
+    }
+  }
+}
+
+void ModAnalysis::genUserCodeModifies(Program *program,
+                                      const std::set<std::string> &bplGlobals) {
+  genSCCs(program);
+  calcModifiesOfSCCs(program);
+  genSCCGraph(program);
+  propagateModifiesUpGraph();
+  addSmackGlobals(bplGlobals);
+  addModifies(program);
+}
+
+bool ModAnalysis::runOnModule(llvm::Module &m) {
+  SmackModuleGenerator &smackGenerator = getAnalysis<SmackModuleGenerator>();
+  Program *program = smackGenerator.getProgram();
+
+  std::set<std::string> bplGlobals;
+  std::vector<std::string> oldBplGlobals = smackGenerator.getBplGlobals();
+  std::copy(oldBplGlobals.begin(), oldBplGlobals.end(),
+            std::inserter(bplGlobals, bplGlobals.end()));
+
+  initProcMap(program);
+
+  if (!bplGlobals.empty()) {
+    genSmackCodeModifies(program, bplGlobals);
+  }
+
+  genUserCodeModifies(program, bplGlobals);
+
+  // DEBUG_WITH_TYPE("bpl", errs() << "" << s.str());
+  return false;
+}
+}
diff --git a/lib/smack/SmackModuleGenerator.cpp b/lib/smack/SmackModuleGenerator.cpp
index 2c70404f4..0672c3d51 100644
--- a/lib/smack/SmackModuleGenerator.cpp
+++ b/lib/smack/SmackModuleGenerator.cpp
@@ -92,6 +92,8 @@ void SmackModuleGenerator::generateProgram(llvm::Module &M) {
     // ... to do below, after memory splitting is determined.
   }
 
+  bplGlobals = rep.getBplGlobals();
+
   auto ds = rep.auxiliaryDeclarations();
   decls.insert(decls.end(), ds.begin(), ds.end());
   decls.insert(decls.end(), rep.getInitFuncs());
diff --git a/share/smack/lib/smack.c b/share/smack/lib/smack.c
index 23692291a..36721eec7 100644
--- a/share/smack/lib/smack.c
+++ b/share/smack/lib/smack.c
@@ -294,8 +294,14 @@ void __SMACK_decls(void) {
   D("function $base(ref) returns (ref);");
   D("var $allocatedCounter: int;\n");
 
+
+#if MEMORY_MODEL_NO_REUSE_IMPLS
+  D("var $Alloc: [ref] bool;");
+  D("function $Size(ref) returns (ref);");
+  D("var $CurrAddr:ref;\n");
+
   D("procedure $malloc(n: ref) returns (p: ref)\n"
-    "modifies $allocatedCounter;\n"
+    "modifies $allocatedCounter, $Alloc, $CurrAddr;\n"
     "{\n"
     "  if ($ne.ref.bool(n, $0.ref)) {\n"
     "    $allocatedCounter := $allocatedCounter + 1;\n"
@@ -303,11 +309,6 @@ void __SMACK_decls(void) {
     "  call p := $$alloc(n);\n"
     "}\n");
 
-#if MEMORY_MODEL_NO_REUSE_IMPLS
-  D("var $Alloc: [ref] bool;");
-  D("function $Size(ref) returns (ref);");
-  D("var $CurrAddr:ref;\n");
-
   D("procedure $galloc(base_addr: ref, size: ref)\n"
     "{\n"
     "  assume $Size(base_addr) == size;\n"
@@ -352,6 +353,16 @@ void __SMACK_decls(void) {
   D("var $Alloc: [ref] bool;");
   D("var $Size: [ref] ref;\n");
 
+  D("procedure $malloc(n: ref) returns (p: ref)\n"
+    "modifies $allocatedCounter, $Alloc, $Size;\n"
+    "{\n"
+    "  if ($ne.ref.bool(n, $0.ref)) {\n"
+    "    $allocatedCounter := $allocatedCounter + 1;\n"
+    "  }\n"
+    "  call p := $$alloc(n);\n"
+    "}\n");
+
+
   D("procedure $galloc(base_addr: ref, size: ref);\n"
     "modifies $Alloc, $Size;\n"
     "ensures $Size[base_addr] == size;\n"
@@ -398,6 +409,16 @@ void __SMACK_decls(void) {
   D("function $Size(ref) returns (ref);");
   D("var $CurrAddr:ref;\n");
 
+  D("procedure $malloc(n: ref) returns (p: ref)\n"
+    "modifies $allocatedCounter, $Alloc, $CurrAddr;\n"
+    "{\n"
+    "  if ($ne.ref.bool(n, $0.ref)) {\n"
+    "    $allocatedCounter := $allocatedCounter + 1;\n"
+    "  }\n"
+    "  call p := $$alloc(n);\n"
+    "}\n");
+
+
   D("procedure $galloc(base_addr: ref, size: ref);\n"
     "modifies $Alloc;\n"
     "ensures $Size(base_addr) == size;\n"
@@ -439,14 +460,16 @@ void __SMACK_decls(void) {
 #endif
 
 #else
+
+#if MEMORY_MODEL_NO_REUSE_IMPLS
+  D("var $CurrAddr:ref;\n");
+
   D("procedure $malloc(n: ref) returns (p: ref)\n"
+    "modifies $CurrAddr;\n"
     "{\n"
     "  call p := $$alloc(n);\n"
     "}\n");
 
-#if MEMORY_MODEL_NO_REUSE_IMPLS
-  D("var $CurrAddr:ref;\n");
-
   D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref)\n"
     "modifies $CurrAddr;\n"
     "{\n"
@@ -468,6 +491,12 @@ void __SMACK_decls(void) {
   D("var $Alloc: [ref] bool;");
   D("var $Size: [ref] ref;\n");
 
+  D("procedure $malloc(n: ref) returns (p: ref)\n"
+    "modifies $Alloc, $Size;\n"
+    "{\n"
+    "  call p := $$alloc(n);\n"
+    "}\n");
+
   D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
     "modifies $Alloc, $Size;\n"
     "ensures $sle.ref.bool($0.ref, n);\n"
@@ -493,6 +522,12 @@ void __SMACK_decls(void) {
 #else // NO_REUSE does not reuse previously-allocated addresses
   D("var $CurrAddr:ref;\n");
 
+  D("procedure $malloc(n: ref) returns (p: ref)\n"
+    "modifies $CurrAddr;\n"
+    "{\n"
+    "  call p := $$alloc(n);\n"
+    "}\n");
+
   D("procedure {:inline 1} $$alloc(n: ref) returns (p: ref);\n"
     "modifies $CurrAddr;\n"
     "ensures $sle.ref.bool($0.ref, n);\n"
diff --git a/share/smack/top.py b/share/smack/top.py
index c7d6ee3c7..043d0eaba 100755
--- a/share/smack/top.py
+++ b/share/smack/top.py
@@ -464,7 +464,7 @@ def verify_bpl(args):
   elif args.verifier == 'boogie' or args.modular:
     command = ["boogie"]
     command += [args.bpl_file]
-    command += ["/nologo", "/noinfer", "/doModSetAnalysis"]
+    command += ["/nologo", "/noinfer"]
     command += ["/timeLimit:%s" % args.time_limit]
     command += ["/errorLimit:%s" % args.max_violations]
     if not args.modular:
diff --git a/tools/llvm2bpl/llvm2bpl.cpp b/tools/llvm2bpl/llvm2bpl.cpp
index 41b97c056..3a61ca6e3 100644
--- a/tools/llvm2bpl/llvm2bpl.cpp
+++ b/tools/llvm2bpl/llvm2bpl.cpp
@@ -36,6 +36,7 @@
 #include "smack/IntegerOverflowChecker.h"
 #include "smack/MemorySafetyChecker.h"
 #include "smack/NormalizeLoops.h"
+#include "smack/ModAnalysis.h"
 #include "smack/RemoveDeadDefs.h"
 #include "smack/SimplifyLibCalls.h"
 #include "smack/SmackModuleGenerator.h"
@@ -229,6 +230,7 @@ int main(int argc, char **argv) {
     F->keep();
     files.push_back(F);
     pass_manager.add(new smack::SmackModuleGenerator());
+    pass_manager.add(new smack::ModAnalysis());
     pass_manager.add(new smack::BplFilePrinter(F->os()));
   }