diff --git a/src/main/scala/uclid/SymbolicSimulator.scala b/src/main/scala/uclid/SymbolicSimulator.scala
index f34ce97e0..b1f156d5e 100644
--- a/src/main/scala/uclid/SymbolicSimulator.scala
+++ b/src/main/scala/uclid/SymbolicSimulator.scala
@@ -313,6 +313,8 @@ class SymbolicSimulator (module : Module) {
             printSMT2(assertionTree, cmd.argObj, solver)
           case "print_module" =>
             UclidMain.println(module.toString)
+          case "dump_c" =>
+            UclidMain.println(module.dumpC)  
           case "set_solver_option" =>
             val option = cmd.args(0)._1.asInstanceOf[lang.StringLit].value
             val value : smt.Context.SolverOption = cmd.args(1)._1 match {
diff --git a/src/main/scala/uclid/lang/ControlCommandChecker.scala b/src/main/scala/uclid/lang/ControlCommandChecker.scala
index d25dee1f3..05f9aa9b0 100644
--- a/src/main/scala/uclid/lang/ControlCommandChecker.scala
+++ b/src/main/scala/uclid/lang/ControlCommandChecker.scala
@@ -176,7 +176,7 @@ class ControlCommandCheckerPass extends ReadOnlyPass[Unit] {
         checkParamIsALogic(cmd, context, filename)
         checkNoArgObj(cmd, filename)
         checkNoResultVar(cmd, filename)
-      case "check" | "print_module" =>
+      case "check" | "print_module" | "dump_c" =>
         checkNoArgs(cmd, filename)
         checkNoParams(cmd, filename)
         checkNoArgObj(cmd, filename)
diff --git a/src/main/scala/uclid/lang/UclidLanguage.scala b/src/main/scala/uclid/lang/UclidLanguage.scala
index ba2b4da55..d7605e675 100644
--- a/src/main/scala/uclid/lang/UclidLanguage.scala
+++ b/src/main/scala/uclid/lang/UclidLanguage.scala
@@ -45,6 +45,7 @@ import scala.collection.mutable.{Map => MutableMap}
 import scala.util.parsing.input.Positional
 import scala.util.parsing.input.Position
 import scala.reflect.ClassTag
+import java.io._
 
 object PrettyPrinter
 {
@@ -161,6 +162,7 @@ object Operator {
 }
 sealed trait Operator extends ASTNode {
   def fixity : Int
+  def dumpC = toString()
   def isPolymorphic = false
   def isTemporal = false
   override val hashBaseId = 32400
@@ -261,45 +263,54 @@ case class IntUnaryMinusOp() extends IntArgOperator {
 // These operators take bitvector operands and return bitvector results.
 sealed abstract class BVArgOperator(val w : Int) extends Operator {
   override def fixity = Operator.INFIX
+  def signed_operands = false
   val arity = 2
 }
 case class BVLTOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = "<"
+  override def signed_operands = true
   override val hashId = 1200
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVLEOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = "<="
+  override def signed_operands = true
   override val hashId = 1201
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVGTOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = ">"
+  override def signed_operands = true
   override val hashId = 1202
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVGEOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = ">="
+  override def signed_operands = true
   override val hashId = 1203
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVLTUOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = "<_u"
+  override def dumpC = "<"
   override val hashId = 1204
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVLEUOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = "<=_u"
+  override def dumpC = "<="
   override val hashId = 1205
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVGTUOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = ">_u"
+  override def dumpC = ">"
   override val hashId = 1206
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVGEUOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = ">=_u"
+  override def dumpC = ">="
   override val hashId = 1207
   override val md5hashCode = computeMD5Hash(w)
 }
@@ -364,28 +375,34 @@ case class BVZeroExtOp(override val w : Int, val e : Int) extends BVArgOperator(
 case class BVLeftShiftBVOp(override val w : Int) extends BVArgOperator(w) {
   override def fixity = Operator.PREFIX
   override def toString = "bv_left_shift"
+  override def dumpC = "<<"
   override val hashId = 1221
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVLRightShiftBVOp(override val w : Int) extends BVArgOperator(w) {
   override def fixity = Operator.PREFIX
   override def toString = "bv_l_right_shift"
+  override def dumpC = ">>"
   override val hashId = 1222
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVARightShiftBVOp(override val w : Int) extends BVArgOperator(w) {
   override def fixity = Operator.PREFIX
   override def toString = "bv_a_right_shift"
+  override def signed_operands = true
+  override def dumpC = ">>"
   override val hashId = 1223
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVUremOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = "%_u"
+  override def dumpC = "%"
   override val hashId = 1224
   override val md5hashCode = computeMD5Hash(w)
 }
 case class BVSremOp(override val w : Int) extends BVArgOperator(w) {
   override def toString = "%"
+  override def signed_operands = true
   override val hashId = 1225
   override val md5hashCode = computeMD5Hash(w)
 }
@@ -406,6 +423,7 @@ case class DisjunctionOp() extends BooleanOperator {
 }
 case class IffOp() extends BooleanOperator {
   override def toString = "<==>"
+  override def dumpC = "=="
   override val hashId = 1302
   override val md5hashCode = computeMD5Hash
 }
@@ -550,6 +568,7 @@ case class ITEOp() extends Operator {
 abstract class BitVectorSlice extends ASTNode {
   def width : Option[Int]
   def isConstantWidth : Boolean
+  def dumpC = toString()
 }
 case class ConstBitVectorSlice(hi: Int, lo: Int) extends BitVectorSlice  {
   Utils.assert(hi >= lo && hi >= 0 && lo >= 0, "Invalid bitvector slice: [" + hi.toString + ":" + lo.toString + "].")
@@ -651,6 +670,7 @@ sealed abstract class Expr extends ASTNode {
   /** Is this value a statically-defined constant? */
   def isConstant = false
   def isTemporal = false
+  def dumpC = toString()
 }
 sealed abstract class PossiblyTemporalExpr extends Expr
 
@@ -672,6 +692,7 @@ sealed abstract class Literal extends Expr {
 /** A non-deterministic new constant. */
 case class FreshLit(typ : Type) extends Literal {
   override def toString = "*"
+  override def dumpC = "nondet()"
   override val hashId = 2200
   override val md5hashCode = computeMD5Hash(typ)
 }
@@ -702,6 +723,7 @@ case class IntLit(value: BigInt) extends NumericLit {
 
 case class BitVectorLit(value: BigInt, width: Int) extends NumericLit {
   override def toString = value.toString + "bv" + width.toString
+  override def dumpC = value.toString
   override def typeOf : NumericType = BitVectorType(width)
   override def to (n : NumericLit) : Seq[NumericLit] = {
     n match {
@@ -736,10 +758,32 @@ case class Tuple(values: List[Expr]) extends Expr {
 //for symbols interpreted by underlying Theory solvers
 case class OperatorApplication(op: Operator, operands: List[Expr]) extends PossiblyTemporalExpr {
   override def isConstant = operands.forall(_.isConstant)
+  override def dumpC = {
+    op match {
+      case PolymorphicSelect(r) =>
+        operands(0).dumpC + "." + r.dumpC
+      case RecordSelect(r) =>
+        operands(0).dumpC + "." + r.dumpC
+      case HyperSelect(i) =>
+        operands(0).dumpC + "." + i
+      case SelectFromInstance(f) =>
+        operands(0).dumpC + "." + f.dumpC
+      case ForallOp(_, _) | ExistsOp(_, _) =>
+        "{" + op.dumpC + operands(0).dumpC + "}"
+      case _ =>
+        if (op.fixity == Operator.INFIX) {
+          "(" + Utils.join(operands.map(_.dumpC), " " + op + " ") + ")"
+        } else if (op.fixity == Operator.PREFIX) {
+          op + "(" + Utils.join(operands.map(_.dumpC), ", ") + ")"
+        } else {
+          "(" + Utils.join(operands.map(_.dumpC), ", ") + ")" + op
+        }
+      }
+  }
   override def toString = {
     op match {
       case PolymorphicSelect(r) =>
-        operands(0).toString + "." + r.toString()
+        operands(0).toString + "." + r.toString
       case RecordSelect(r) =>
         operands(0).toString + "." + r.toString
       case HyperSelect(i) =>
@@ -776,6 +820,7 @@ case class Lambda(ids: List[(Identifier,Type)], e: Expr) extends Expr {
 
 sealed abstract class Lhs(val ident: Identifier) extends ASTNode {
   def isProceduralLhs : Boolean
+  def dumpC = toString()
 }
 case class LhsId(id: Identifier) extends Lhs(id) {
   override def toString = id.toString
@@ -887,6 +932,7 @@ sealed abstract class Type extends PositionedNode {
   def ids = List.empty[Identifier]
   def matches (t2 : Type) = (this == t2)
   def defaultValue : Option[Expr] = None
+  def dumpC = toString()
 }
 
 /**
@@ -927,6 +973,7 @@ case class BooleanType() extends PrimitiveType {
   override def defaultValue = Some(BoolLit(false))
   override val hashId = 2702
   override val md5hashCode = computeMD5Hash
+  override def dumpC = "bool"
 }
 case class IntegerType() extends NumericType {
   override def toString = "integer"
@@ -934,10 +981,12 @@ case class IntegerType() extends NumericType {
   override def defaultValue = Some(IntLit(0))
   override val hashId = 2703
   override val md5hashCode = computeMD5Hash
+  override def dumpC = "int"
 }
 case class BitVectorType(width: Int) extends NumericType {
   override def toString = "bv" + width.toString
   override def isBitVector = true
+  override def dumpC = "__CPROVER_bitvector["+ width.toString+"]"
   def isValidSlice(slice : ConstBitVectorSlice) : Boolean = {
     return (slice.lo >= 0 && slice.hi < width)
   }
@@ -1000,6 +1049,7 @@ abstract sealed class ProductType extends Type {
 case class TupleType(fieldTypes: List[Type]) extends ProductType {
   override def fields = fieldTypes.zipWithIndex.map(p  => (Identifier("_" + (p._2+1).toString), p._1))
   override def toString = "{" + Utils.join(fieldTypes.map(_.toString), ", ") + "}"
+  override def dumpC = "struct {" + Utils.join(fields.map((f) => f._2.dumpC + " " + f._1.dumpC), "; ")  + ";}"
   override def isTuple = true
   override def defaultValue = {
     val defaults = fieldTypes.map(_.defaultValue).flatten
@@ -1016,6 +1066,7 @@ case class TupleType(fieldTypes: List[Type]) extends ProductType {
 case class RecordType(members : List[(Identifier,Type)]) extends ProductType {
   override def fields = members
   override def toString = "record {" + Utils.join(fields.map((f) => f._1.toString + " : " + f._2.toString), ", ")  + "}"
+  override def dumpC = "struct {" + Utils.join(fields.map((f) => f._2.dumpC + " " + f._1.dumpC), "; ")  + ";}"
   override def isRecord = true
   override def matches(t2 : Type) : Boolean = {
     t2 match {
@@ -1138,15 +1189,18 @@ case class HavocableInstanceId(opapp : OperatorApplication) extends HavocableEnt
 /** Statements **/
 sealed abstract class Statement extends ASTNode {
   override def toString = Utils.join(toLines, "\n") + "\n"
+  def dumpC = Utils.join(toCLines, "\n")+"\n"
   def hasStmtBlock = false
   val isLoop = false
   val hasLoop = false
   val hasCall : Boolean
   val hasInternalCall : Boolean
   def toLines : List[String]
+  def toCLines = toLines
 }
 case class SkipStmt() extends Statement {
   override def toLines = List("skip; // " + position.toString)
+  override def toCLines = List("// skip;")
   override val hasCall = false
   override val hasInternalCall = false
   override val hashId = 3000
@@ -1154,6 +1208,7 @@ case class SkipStmt() extends Statement {
 }
 case class AssertStmt(e: Expr, id : Option[Identifier]) extends Statement {
   override def toLines = List("assert " + e + "; // " + position.toString)
+  override def toCLines = List("assert( " + e + "); // " + position.toString)
   override val hasCall = false
   override val hasInternalCall = false
   override val hashId = 3001
@@ -1161,6 +1216,7 @@ case class AssertStmt(e: Expr, id : Option[Identifier]) extends Statement {
 }
 case class AssumeStmt(e: Expr, id : Option[Identifier]) extends Statement {
   override def toLines = List("assume " + e + "; // " + position.toString)
+  override def toCLines = List("assume (" + e + "); // " + position.toString)
   override val hasCall = false
   override val hasInternalCall = false
   override val hashId = 3002
@@ -1168,6 +1224,7 @@ case class AssumeStmt(e: Expr, id : Option[Identifier]) extends Statement {
 }
 case class HavocStmt(havocable : HavocableEntity) extends Statement {
   override def toLines = List("havoc " + havocable.toString() + "; // " + position.toString)
+  override def toCLines = List("havoc (" + havocable.toString() + "); // " + position.toString)
   override val hasCall = false
   override val hasInternalCall = false;
   override val hashId = 3003
@@ -1176,6 +1233,8 @@ case class HavocStmt(havocable : HavocableEntity) extends Statement {
 case class AssignStmt(lhss: List[Lhs], rhss: List[Expr]) extends Statement {
   override def toLines =
     List(Utils.join(lhss.map (_.toString), ", ") + " = " + Utils.join(rhss.map(_.toString), ", ") + "; // " + position.toString)
+  override def toCLines  =
+    List(Utils.join(lhss.map (_.dumpC), ", ") + " = " + Utils.join(rhss.map(_.dumpC), ", ") + "; // " + position.toString)  
   override val hasCall = false
   override val hasInternalCall = false
   override val hashId = 3004
@@ -1190,6 +1249,11 @@ case class BlockStmt(vars: List[BlockVarsDecl], stmts: List[Statement]) extends
       stmts.flatMap(_.toLines).map(PrettyPrinter.indent(1) + _) ++
     List("}")
   }
+  override def toCLines  = {
+      vars.map(PrettyPrinter.indent(1) + _.dumpC) ++
+      stmts.flatMap(_.toCLines).map(PrettyPrinter.indent(1) + _)
+  }
+
   override val hasCall = stmts.exists(st => st.hasCall)
   override val hasInternalCall = stmts.exists(st => st.hasInternalCall)
   override val hashId = 3005
@@ -1205,6 +1269,13 @@ case class IfElseStmt(cond: Expr, ifblock: Statement, elseblock: Statement) exte
     elseblock.toLines.map(PrettyPrinter.indent(1) + _)
   }
   override def toLines = lines
+  lazy val clines : List[String] = {
+    List("if(%s)".format(cond.toString())) ++
+    ifblock.toCLines.map(PrettyPrinter.indent(1) + _) ++
+    List("else") ++
+    elseblock.toCLines.map(PrettyPrinter.indent(1) + _)
+  }
+  override def toCLines = clines
   override val hasCall = ifblock.hasCall || elseblock.hasCall
   override val hasInternalCall = ifblock.hasInternalCall || elseblock.hasInternalCall
   override val hashId = 3006
@@ -1220,6 +1291,11 @@ case class ForStmt(id: Identifier, typ : Type, range: (Expr,Expr), body: Stateme
     val forLine = "for " + id + " in range(" + range._1 +"," + range._2 + ") {  // " + position.toString
     List(forLine) ++ body.toLines.map(PrettyPrinter.indent(1) + _) ++ List("}")
   }
+    override def toCLines = {
+    val forLine = "for " + typ.toString() + id + " in range(" + range._1 +"," + range._2 + ") {  // " + position.toString
+    List(forLine) ++ body.toCLines.map(PrettyPrinter.indent(1) + _) ++ List("}")
+  }
+
   override val hasCall = body.hasCall
   override val hasInternalCall = body.hasInternalCall
   override val hashId = 3007
@@ -1236,6 +1312,7 @@ case class WhileStmt(cond: Expr, body: Statement, invariants: List[Expr])
     val invLines = invariants.map(inv => PrettyPrinter.indent(1) + "invariant " + inv.toString() + "; // " + inv.position.toString())
     List(headLine) ++ invLines ++ body.toLines.map(PrettyPrinter.indent(1) + _)
   }
+
   override val hasCall = body.hasCall
   override val hasInternalCall = body.hasInternalCall
   override val hashId = 3008
@@ -1270,6 +1347,7 @@ case class ModuleCallStmt(id: Identifier) extends Statement {
 case class BlockVarsDecl(ids : List[Identifier], typ : Type) extends ASTNode {
   override def toString = "var " + Utils.join(ids.map(id => id.toString()), ", ") +
                           " : " + typ.toString() + "; // " + typ.position.toString()
+  def dumpC = typ.dumpC + " "+ Utils.join(ids.map(id => id.toString()), ", ") + "; //" + typ.position.toString()                     
   override val hashId = 3100
   override val md5hashCode = computeMD5Hash(ids, typ)
 }
@@ -1319,6 +1397,8 @@ case class FunctionSig(args: List[(Identifier,Type)], retType: Type) extends AST
 sealed abstract class Decl extends ASTNode {
   def declNames : List[Identifier]
   val hashId : Int
+  def dumpC = toString()
+  def dumpC_assumption = toString()
 }
 
 case class InstanceDecl(instanceId : Identifier, moduleId : Identifier, arguments: List[(Identifier, Option[Expr])], instType : Option[ModuleInstanceType], modType : Option[ModuleType]) extends Decl
@@ -1395,24 +1475,28 @@ case class ModifiableInstanceId(opapp : OperatorApplication) extends ModifiableE
 
 sealed abstract class ProcedureVerificationExpr extends ASTNode {
   val expr : Expr
+  def dumpC = toString
 }
 case class ProcedureRequiresExpr(e : Expr) extends ProcedureVerificationExpr {
   override val expr = e
   override val toString = "requires " + e.toString()
   override val hashId = 3400
   override val md5hashCode = computeMD5Hash(e)
+  override val dumpC = "__CPROVER_assume(" + e.toString() + ");\n"
 }
 case class ProcedureEnsuresExpr(e : Expr) extends ProcedureVerificationExpr {
   override val expr = e
   override val toString = "ensures " + e.toString()
   override val hashId = 3401
   override val md5hashCode = computeMD5Hash(e)
+  override val dumpC = "assert(" + e.toString() + ");\n"
 }
 case class ProcedureModifiesExpr(modifiable : ModifiableEntity) extends ProcedureVerificationExpr {
   override val expr = modifiable.expr
   override val toString = "modifies " + modifiable.toString
   override val hashId = 3402
   override val md5hashCode = computeMD5Hash(modifiable)
+  override val dumpC = ""
 }
 
 case class ProcedureAnnotations(ids : Set[Identifier]) extends ASTNode {
@@ -1432,6 +1516,7 @@ case class ProcedureDecl(
     requires: List[Expr], ensures: List[Expr], modifies: Set[ModifiableEntity],
     annotations : ProcedureAnnotations) extends Decl
 {
+  val procedureName = id
   override val hashId = 3902
   override val md5hashCode = computeMD5Hash(id, sig, body, requires, ensures, modifies.toList, annotations)
   override def toString = {
@@ -1444,6 +1529,18 @@ case class ProcedureDecl(
     Utils.join(ensures.map(PrettyPrinter.indent(2) + "ensures " + _.toString + "; \n"), "") +
     Utils.join(body.toLines.map(PrettyPrinter.indent(2) + _), "\n")
   }
+  override def dumpC = {
+    val declareVars = sig.inParams.foldLeft("")
+    {case (acc,i) => acc + PrettyPrinter.indent(1)+ i._2.dumpC + " " + i._1.dumpC + ";\n" + PrettyPrinter.indent(1) + "havoc(" + i._1 + ");\n" }
+    val declareOutputVars = sig.outParams.foldLeft("")
+        {case (acc,i) => acc + PrettyPrinter.indent(1)+ i._2.dumpC + " " + i._1.dumpC + ";\n" + PrettyPrinter.indent(1) + "havoc(" + i._1 + ");\n" }
+
+    "void " + "verify_"+id + "() {\n" + declareVars + declareOutputVars +
+    Utils.join(requires.map(PrettyPrinter.indent(2) + "__CPROVER_assume" + _.dumpC + ";\n"), "") +
+    Utils.join(body.toCLines.map(PrettyPrinter.indent(2) + _), "\n") + "\n" + 
+    Utils.join(ensures.map(PrettyPrinter.indent(2) + "assert" + _.dumpC + "; \n"), "") +
+    "}\n"
+  }
   override def declNames = List(id)
   def hasPrePost = requires.size > 0 || ensures.size > 0
   val shouldInline =
@@ -1455,6 +1552,7 @@ case class TypeDecl(id: Identifier, typ: Type) extends Decl {
   override val md5hashCode = computeMD5Hash(id, typ)
   override def toString = "type " + id + " = " + typ + "; // " + position.toString
   override def declNames = List(id)
+  override def dumpC = "typedef " + typ.dumpC + " " + id + ";"
 }
 case class ModuleTypesImportDecl(id : Identifier) extends Decl {
   override val hashId = 3904
@@ -1466,6 +1564,7 @@ case class StateVarsDecl(ids: List[Identifier], typ: Type) extends Decl {
   override val hashId = 3905
   override val md5hashCode = computeMD5Hash(ids, typ)
   override def toString = "var " + Utils.join(ids.map(_.toString), ", ") + " : " + typ + "; // " + position.toString
+  override def dumpC = typ.dumpC +" "+ Utils.join(ids.map(_.toString), ", ") + "; // " + position.toString 
   override def declNames = ids
 }
 case class InputVarsDecl(ids: List[Identifier], typ: Type) extends Decl {
@@ -1496,6 +1595,7 @@ case class ConstantLitDecl(id : Identifier, lit : NumericLit) extends Decl {
   override val md5hashCode = computeMD5Hash(id, lit)
   override def toString = "const %s = %s; // %s".format(id.toString(), lit.toString(), position.toString())
   override def declNames = List(id)
+ // override def dumpC = "const %s = %s; // %s".format(id.dumpC, lit.dumpC, position.toString())
 }
 case class ConstantsDecl(ids: List[Identifier], typ: Type) extends Decl with ModuleExternal {
   override val hashId = 3910
@@ -1504,6 +1604,7 @@ case class ConstantsDecl(ids: List[Identifier], typ: Type) extends Decl with Mod
   override def declNames = ids
   override def extNames = ids
   override def extType = typ
+  override def dumpC = "const" + typ.dumpC +" "+ Utils.join(ids.map(_.toString), ", ") + "; // " + position.toString
 }
 case class ModuleConstantsImportDecl(id: Identifier) extends Decl {
   override val hashId = 3919 
@@ -1591,6 +1692,7 @@ case class LetVariableTerm(typ: Type) extends GrammarTerm {
 }
 case class VariableTerm(typ: Type) extends GrammarTerm {
   override def toString = "var " + typ.toString()
+  def dumpC = typ.dumpC + " "
   override val hashId = 4007
   override val md5hashCode = computeMD5Hash(typ)
 }
@@ -1638,6 +1740,8 @@ case class InitDecl(body: Statement) extends Decl {
   override def toString =
     "init // " + position.toString + "\n" +
     Utils.join(body.toLines.map(PrettyPrinter.indent(2) + _), "\n")
+  override def dumpC =
+    Utils.join(body.toCLines.map(PrettyPrinter.indent(2) + _), "\n")  
   override def declNames = List.empty
 }
 case class NextDecl(body: Statement) extends Decl {
@@ -1646,6 +1750,10 @@ case class NextDecl(body: Statement) extends Decl {
   override def toString =
     "next // " + position.toString + "\n" +
     Utils.join(body.toLines.map(PrettyPrinter.indent(2) + _), "\n")
+  override def dumpC =  
+    Utils.join(body.toCLines.map(PrettyPrinter.indent(2) + _), "\n") 
+    
+
   override def declNames = List.empty
 }
 case class SpecDecl(id: Identifier, expr: Expr, params: List[ExprDecorator]) extends Decl {
@@ -1664,6 +1772,8 @@ case class SpecDecl(id: Identifier, expr: Expr, params: List[ExprDecorator]) ext
     }
     "%s %s%s : %s; // %s".format(propertyKeyword, id.toString, declString, expr.toString, position.toString)
   }
+  override def dumpC = "assert("+ expr.dumpC + ");\n"
+  override def dumpC_assumption = "__CPROVER_assume("+expr.dumpC +");\n"
   override def declNames = List(id)
   def name = "%s %s".format(propertyKeyword, id.toString())
 }
@@ -1678,6 +1788,12 @@ case class AxiomDecl(id : Option[Identifier], expr: Expr, params: List[ExprDecor
       case None => "axiom " + expr.toString
     }
   }
+  override def dumpC = {
+     id match {
+      case Some(id) => "__CPROVER_assume(" + id.dumpC + " : " + expr.dumpC +");\n"
+      case None => "__CPROVER_assume( " + expr.dumpC + ");\n"
+     }
+  }
   override def declNames = id match {
     case Some(i) => List(i)
     case _ => List.empty
@@ -1721,6 +1837,7 @@ case class GenericProofCommand(
     }
   }
   def isVerify : Boolean = { name == Identifier("verify") }
+
   override def toString = {
     val nameStr = name.toString
     val paramStr = if (params.size > 0) { "[" + Utils.join(params.map(_.toString), ", ") + "]" } else { "" }
@@ -1729,6 +1846,33 @@ case class GenericProofCommand(
     val objStr = argObj match { case Some(id) => id.toString + "->"; case None => "" }
     resultStr + objStr + nameStr + paramStr + argStr + ";" + " // " + position.toString
   }
+
+  def dumpC = {
+    name match{
+      case Identifier("verify") => ""// do nothing here. 
+      case Identifier("induction") => 
+      "void induction(void){\nhavoc_all();\n" + 
+      PrettyPrinter.indent(1) + "init();\n" + 
+      PrettyPrinter.indent(1) + "assert_properties();\n" +
+      PrettyPrinter.indent(1) + "havoc_all();\nassume_properties();\n" + 
+      PrettyPrinter.indent(1) + "next();\n" + 
+      PrettyPrinter.indent(1) + "assert_properties();\n" +
+      "}\n"; 
+      case Identifier("unroll")=>
+      val iterations=args(0)._2;
+      "void unroll(void){\nhavoc_all();\n" +
+      PrettyPrinter.indent(1) + "init();\n" + 
+      PrettyPrinter.indent(1) + "assert_properties();\n" +
+      PrettyPrinter.indent(1) + "for(int i=0; i<" + iterations+ " ;i++){\n" +
+      PrettyPrinter.indent(2) + "next();\n" + 
+      PrettyPrinter.indent(2) + "assert_properties();\n" +
+      PrettyPrinter.indent(1) + "}\n" +
+      "}\n"
+      case Identifier("bmc")=>"unroll: not able to dump C for LTL properties"
+      case Identifier("check") | Identifier("print_results") |Identifier("print_cex") | Identifier("dump_c") | Identifier("print_module")  =>""
+      case _ => "not able to dump C for this property"
+    }
+  }
   override val hashId = 4200
   override val md5hashCode = computeMD5Hash(name, params, args, resultVar, argObj)
 }
@@ -1809,6 +1953,7 @@ case class Module(id: Identifier, decls: List[Decl], cmds : List[GenericProofCom
   // module state variables.
   lazy val vars : List[(Identifier, Type)] =
     decls.collect { case vars : StateVarsDecl => vars }.flatMap(v => v.ids.map(id => (id, v.typ)))
+  
   lazy val sharedVars: List[(Identifier, Type)] =
     decls.collect { case sVars : SharedVarsDecl => sVars }.flatMap(sVar => sVar.ids.map(id => (id, sVar.typ)))
   lazy val constLits: List[(Identifier, NumericLit)] =
@@ -1900,6 +2045,84 @@ case class Module(id: Identifier, decls: List[Decl], cmds : List[GenericProofCom
     Module(id, decls, cmds, newNotes)
   }
 
+
+
+  def dumpC = 
+  {
+    val file = new File("UCLID_dump_C.c")
+    val bw = new BufferedWriter(new FileWriter(file))
+    lazy val varDecls = decls.filter(_.isInstanceOf[StateVarsDecl])
+    lazy val initDecl = decls.filter(_.isInstanceOf[InitDecl])
+    lazy val nextDecl = decls.filter(_.isInstanceOf[NextDecl])
+    lazy val propertyDecls = decls.filter(_.isInstanceOf[SpecDecl])
+    lazy val typeDecls = decls.filter(_.isInstanceOf[TypeDecl])
+    lazy val procedureDecls = decls.filter(_.isInstanceOf[ProcedureDecl])
+    var usedProcedures : Set[String] = Set()
+
+    for (cmd <- cmds if cmd.name == Identifier("verify"))
+      usedProcedures+= cmd.args(0)._2 
+
+    
+   
+    var cmdCalls : String  = ""
+
+    val havoc = 
+    "void havoc_all(){\n" +
+    varDecls.foldLeft("") { case (acc,i) => acc + PrettyPrinter.indent(1) + 
+      i.declNames.foldLeft("") {case (acc, i) => acc + PrettyPrinter.indent(1) + "__CPROVER_havoc(" + i.dumpC + ");\n" }} +
+    "}\n"
+    val assert_property = 
+    "void assert_properties(){\n"+
+    propertyDecls.foldLeft(""){case (acc,i) => acc + PrettyPrinter.indent(1) + i.dumpC + "\n" } + "}\n"
+
+    val assume_property = 
+    "void assume_properties(){\n"+
+    propertyDecls.foldLeft(""){case (acc,i) => acc + PrettyPrinter.indent(1) + i.dumpC_assumption + "\n" } + "}\n"
+
+    def getCmdString(cmd: GenericProofCommand):String = {
+      cmd.name match {
+         case Identifier("verify") => cmdCalls += "verify_"+cmd.args(0)._2 + "();\n"
+         case Identifier("unroll") => cmdCalls += "unroll();\n";
+         case Identifier("induction") => cmdCalls += "induction();\n"
+         case _ => // do nothing
+      }
+      cmd.dumpC
+    }
+
+  bw.write("// C code generated by UCLID5 \n")
+  bw.write("// WARNING: all integer types are printed as C integers\n") 
+  bw.write("#include \"stdbool.h\"\n") 
+  bw.write("// global variables \n")  
+  bw.flush()
+  bw.write( varDecls.foldLeft("") { case (acc,i) => acc + PrettyPrinter.indent(1) + i.dumpC + "\n" } + "\n" )
+  bw.write(havoc + assert_property + assume_property) 
+  bw.flush()
+  bw.write("void init()" + "{\n" +
+  initDecl.foldLeft("") { case (acc,i) => acc + PrettyPrinter.indent(1) + i.dumpC + "\n" } + 
+  "}\n\nvoid next()"+"{\n")
+  bw.flush()
+  bw.write(nextDecl.foldLeft("") { case (acc,i) => acc + PrettyPrinter.indent(1) + i.dumpC + "\n" } + 
+  "}\n")
+  bw.flush()
+// print procedures
+  for(procedure <- procedureDecls)
+  {
+    if(usedProcedures.contains(procedure.asInstanceOf[ProcedureDecl].procedureName.toString))
+    {
+      bw.write(procedure.dumpC + "\n")
+      bw.flush()
+    }
+  }
+
+  bw.write(cmds.foldLeft("") { case (acc,i) => acc + PrettyPrinter.indent(1) + getCmdString(i) }) 
+  bw.write("\nvoid main() {\n" +  
+  PrettyPrinter.indent(1) + cmdCalls + "\n}\n")
+  bw.flush()
+  bw.close()
+  "Printed C code to UCLID_dump_C.c"
+  }
+
+
   override def toString =
     "\nmodule " + id + " {\n" +
       decls.foldLeft("") { case (acc,i) => acc + PrettyPrinter.indent(1) + i + "\n" } +