diff --git a/col/src/main/java/vct/col/ast/expr/constant/ConstantExpression.scala b/col/src/main/java/vct/col/ast/expr/constant/ConstantExpression.scala
index f8ef894cae..ea0b5e030f 100644
--- a/col/src/main/java/vct/col/ast/expr/constant/ConstantExpression.scala
+++ b/col/src/main/java/vct/col/ast/expr/constant/ConstantExpression.scala
@@ -15,12 +15,14 @@ import vct.col.ast.util.{ASTMapping, ASTMapping1, ASTVisitor, VisitorHelper}
 case class ConstantExpression(val value:Value) extends ASTNode with VisitorHelper {
   def this(v:Value, t:Type) = { this(v); setType(t) }
   def this(v:Value, t:Type, origin:Origin) = { this(v, t); setOrigin(origin) }
+  def this(i:BigInt) = this(new IntegerValue(i), new PrimitiveType(PrimitiveSort.Integer))
   def this(i:Int) = this(new IntegerValue(i), new PrimitiveType(PrimitiveSort.Integer))
   def this(b:Boolean) = this(new BooleanValue(b), new PrimitiveType(PrimitiveSort.Boolean))
   def this(s:String) = this(new StringValue(s), new PrimitiveType(PrimitiveSort.String))
   def this(l:Long) = this(new LongValue(l), new PrimitiveType(PrimitiveSort.Long))
 	def this(d:Double) = this(new DoubleValue(d), new PrimitiveType(PrimitiveSort.Double))
 
+  def this(i:BigInt, origin: Origin) = { this(i); setOrigin(origin); }
   def this(i:Int, origin:Origin) = { this(i); setOrigin(origin) }
   def this(b:Boolean, origin:Origin) = { this(b); setOrigin(origin) }
   def this(s:String, origin:Origin) = { this(s); setOrigin(origin) }
diff --git a/col/src/main/java/vct/col/ast/expr/constant/IntegerValue.scala b/col/src/main/java/vct/col/ast/expr/constant/IntegerValue.scala
index e9c8b2058b..4cf2543b2a 100644
--- a/col/src/main/java/vct/col/ast/expr/constant/IntegerValue.scala
+++ b/col/src/main/java/vct/col/ast/expr/constant/IntegerValue.scala
@@ -2,9 +2,20 @@ package vct.col.ast.expr.constant
 
 import scala.annotation.nowarn
 
+object IntegerValue {
+  def unapply(iv: IntegerValue): Option[Int] = iv.toInt()
+}
+
 /** Represents a constant integer with value "`value`". */
 @nowarn("msg=.*comparing values of types Any and .* using `equals`.*")
-case class IntegerValue(val value:Int) extends Value {
-  override def toString() = Integer.toString(value)
+case class IntegerValue(val value:BigInt) extends Value {
+
+  override def toString() = value.toString()
   override def equals(o:Any) = o.equals(value)
+
+  def toInt(): Option[Int] = if (BigInt(Integer.MIN_VALUE) <= value && value <= BigInt(Integer.MAX_VALUE)) {
+    Some(value.toInt)
+  } else {
+    None
+  }
 }
diff --git a/col/src/main/java/vct/col/ast/util/ASTFactory.java b/col/src/main/java/vct/col/ast/util/ASTFactory.java
index c8e82faa84..7b1cb6efb3 100644
--- a/col/src/main/java/vct/col/ast/util/ASTFactory.java
+++ b/col/src/main/java/vct/col/ast/util/ASTFactory.java
@@ -4,6 +4,7 @@
 import java.util.*;
 import java.util.Map.Entry;
 
+import scala.math.BigInt;
 import vct.col.ast.expr.*;
 import vct.col.ast.expr.constant.ConstantExpression;
 import vct.col.ast.expr.constant.StructValue;
@@ -232,6 +233,9 @@ public ConstantExpression constant(double i) {
   public ConstantExpression constant(int i) {
     return constant(origin_stack.get(),i);
   }
+  public ConstantExpression constant(BigInt i) {
+    return constant(origin_stack.get(),i);
+  }
   public ConstantExpression constant(long i) {
     return constant(origin_stack.get(),i);
   }
@@ -243,6 +247,14 @@ public ConstantExpression constant(Origin origin, boolean b) {
     res.accept_if(post);
     return res;    
   }
+  /**
+   * Create a new biginteger constant
+   */
+  public ConstantExpression constant(Origin origin, BigInt bi) {
+    ConstantExpression res=new ConstantExpression(bi,origin);
+    res.accept_if(post);
+    return res;
+  }
   /**
    * Create a new double constant.
    */
diff --git a/examples/basic/BigInts.pvl b/examples/basic/BigInts.pvl
new file mode 100644
index 0000000000..ded72f951a
--- /dev/null
+++ b/examples/basic/BigInts.pvl
@@ -0,0 +1,14 @@
+//:: cases BigInts
+//:: tools silicon carbon
+
+class C {
+  static boolean int32r(int v) =
+    -2147483648 <= v && v <= 2147483647;
+
+  static int foo() = -9999999999999999999999;
+  static int bar() = 9999999999999999999999;
+
+  requires foo() < bar();
+  requires 1111111111111111 < 2222222222222222222222;
+  void m() { }
+}
\ No newline at end of file
diff --git a/parsers/src/main/java/vct/parsers/PVLtoCOL.scala b/parsers/src/main/java/vct/parsers/PVLtoCOL.scala
index 3bbeb926eb..eede6106b4 100644
--- a/parsers/src/main/java/vct/parsers/PVLtoCOL.scala
+++ b/parsers/src/main/java/vct/parsers/PVLtoCOL.scala
@@ -386,7 +386,7 @@ case class PVLtoCOL(fileName: String, tokens: CommonTokenStream, parser: PVLPars
     case NonTargetUnit12("id", "(", exp, ")") => expr(exp)
     case NonTargetUnit13("|", seq, "|") => create expression(Size, expr(seq))
     case NonTargetUnit14("?", id) => create expression(BindOutput, convertIDName(id))
-    case NonTargetUnit15(num) => create constant Integer.parseInt(num)
+    case NonTargetUnit15(num) => create constant BigInt(num)
     case NonTargetUnit16(seq) => ??(tree)
     case NonTargetUnit17("(", exp, ")") => expr(exp)
     case NonTargetUnit18(id) => convertIDName(id)
diff --git a/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java b/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
index f568616c66..9940fffc79 100644
--- a/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
+++ b/src/main/java/vct/col/rewrite/ParallelBlockEncoder.java
@@ -432,14 +432,14 @@ private void gen_consistent(ParallelRegion region, ParallelBlock pb1, ParallelBl
   
   private int ConstantExpToInt(ConstantExpression e)
   { 
-    return ((IntegerValue)e.value()).value();
+    return (int) ((IntegerValue)e.value()).toInt().get();
     
   }  
   private boolean sidecondition_check(ASTSpecial e)  {
      ///1. check the distance of dependence constant expressions    
       if(e.getArg(2) instanceof ConstantExpression)
-      {                                                           
-        return ConstantExpToInt((ConstantExpression)e.getArg(2)) > 0 ;            
+      {
+        return ConstantExpToInt((ConstantExpression)e.getArg(2)) > 0 ;
       } else{
         return false;       
       }                     
@@ -920,7 +920,7 @@ protected void check_send_recv(DeclarationStatement[] body_decl, String var_name
   
   private int getConstant(ASTNode arg) {
     IntegerValue v = (IntegerValue)((ConstantExpression)arg).value();
-    return v.value();
+    return (int) v.toInt().get();
   }
 
   @Override
diff --git a/viper/src/main/java/viper/api/ExpressionFactory.java b/viper/src/main/java/viper/api/ExpressionFactory.java
index dbb923c55a..2bd63ac5fd 100644
--- a/viper/src/main/java/viper/api/ExpressionFactory.java
+++ b/viper/src/main/java/viper/api/ExpressionFactory.java
@@ -1,6 +1,7 @@
 package viper.api;
 
 import hre.util.Triple;
+import scala.math.BigInt;
 
 import java.util.List;
 import java.util.Map;
@@ -17,6 +18,7 @@ public interface ExpressionFactory<O,T,E> {
 
   /** Create an integer constant. */
   E Constant(O o, int i);
+  E Constant(O o, BigInt i);
 
   /** Create a boolean constant. */
   E Constant(O o, boolean b);
diff --git a/viper/src/main/java/viper/api/SilverExpressionMap.java b/viper/src/main/java/viper/api/SilverExpressionMap.java
index d392286747..ced8ca2309 100644
--- a/viper/src/main/java/viper/api/SilverExpressionMap.java
+++ b/viper/src/main/java/viper/api/SilverExpressionMap.java
@@ -10,6 +10,7 @@
 import static hre.lang.System.Abort;
 
 import hre.util.Triple;
+import scala.math.BigInt;
 import vct.col.ast.expr.*;
 import vct.col.ast.expr.constant.BooleanValue;
 import vct.col.ast.expr.constant.ConstantExpression;
@@ -59,15 +60,20 @@ public E map(StandardProcedure p) {
   @Override
   public E map(ConstantExpression e) {
     if (e.value() instanceof IntegerValue) {
-      int v = ((IntegerValue) e.value()).value();
+      boolean isInIntRange = ((IntegerValue) e.value()).toInt().isDefined();
+      BigInt v = ((IntegerValue) e.value()).value();
       if (e.getType().isFraction()) {
-        switch (v) {
-          case 0:
-            return create.no_perm(e.getOrigin());
-          case 1:
-            return create.write_perm(e.getOrigin());
-          default:
-            return create.frac(e.getOrigin(), create.Constant(e.getOrigin(), v), create.Constant(e.getOrigin(), 1));
+        if (isInIntRange && (v.intValue() == 0 || v.intValue() == 1)) {
+          switch (v.intValue()) {
+            case 0:
+              return create.no_perm(e.getOrigin());
+            case 1:
+              return create.write_perm(e.getOrigin());
+            default:
+              return null;
+          }
+        } else {
+          return create.frac(e.getOrigin(), create.Constant(e.getOrigin(), v), create.Constant(e.getOrigin(), 1));
         }
       } else {
         return create.Constant(e.getOrigin(), v);
diff --git a/viper/src/main/java/viper/api/VerCorsExpressionFactory.java b/viper/src/main/java/viper/api/VerCorsExpressionFactory.java
index 2dfbb7a03b..79a56f465c 100644
--- a/viper/src/main/java/viper/api/VerCorsExpressionFactory.java
+++ b/viper/src/main/java/viper/api/VerCorsExpressionFactory.java
@@ -8,6 +8,7 @@
 import hre.ast.Origin;
 import hre.lang.HREError;
 import hre.util.Triple;
+import scala.math.BigInt;
 import vct.col.ast.generic.ASTNode;
 import vct.col.ast.type.ASTReserved;
 import vct.col.ast.stmt.decl.DeclarationStatement;
@@ -134,6 +135,13 @@ public ASTNode Constant(Origin o, int i) {
     return res;
   }
 
+  @Override
+  public ASTNode Constant(Origin o, BigInt bi) {
+    enter(o);
+    ASTNode res = create.constant(bi);
+    leave();
+    return res;
+  }
 
   @Override
   public ASTNode current_perm(Origin o, ASTNode expr){
diff --git a/viper/src/main/scala/viper/api/SilverExpressionFactory.scala b/viper/src/main/scala/viper/api/SilverExpressionFactory.scala
index 5e7a0575e6..be3e418042 100644
--- a/viper/src/main/scala/viper/api/SilverExpressionFactory.scala
+++ b/viper/src/main/scala/viper/api/SilverExpressionFactory.scala
@@ -14,6 +14,7 @@ import hre.util
 class SilverExpressionFactory[O] extends ExpressionFactory[O,Type,Exp] with FactoryUtils[O] {
    
   override def Constant(o:O, i:Int): Exp = IntLit(i)(NoPosition,new OriginInfo(o))
+  override def Constant(o:O, bi:BigInt): Exp = IntLit(bi)(NoPosition,new OriginInfo(o))
   override def Constant(o:O, b:Boolean): Exp =
     if(b) TrueLit()(NoPosition,new OriginInfo(o)) else FalseLit()(NoPosition,new OriginInfo(o))