diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright (c) 2013-2014, Ranjit Jhala
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Ranjit Jhala nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/liquid-finfield.cabal b/liquid-finfield.cabal
new file mode 100644
--- /dev/null
+++ b/liquid-finfield.cabal
@@ -0,0 +1,21 @@
+cabal-version:      1.24
+name:               liquid-finfield
+version:            0.9.12.2.1
+synopsis:           Finite field utilities for LiquidHaskell (requires cvc5)
+description:        Finite field utilities for LiquidHaskell (requires cvc5)
+license:            BSD3
+license-file:       LICENSE
+copyright:          2010-19 Ranjit Jhala & Niki Vazou & Eric L. Seidel, University of California, San Diego.
+author:             Alex Gryzlov, Niki Vazou
+maintainer:         Ranjit Jhala <jhala@cs.ucsd.edu>
+category:           Language
+homepage:           https://github.com/ucsd-progsys/liquidhaskell
+build-type:         Simple
+
+library
+  exposed-modules:  Language.Haskell.Liquid.FinField
+                    Language.Haskell.Liquid.FinField.FF17
+  hs-source-dirs:     src
+  build-depends:      base          < 5
+                    , liquidhaskell        >= 0.9.12.2.1
+  default-language:   Haskell2010
diff --git a/src/Language/Haskell/Liquid/FinField.hs b/src/Language/Haskell/Liquid/FinField.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Liquid/FinField.hs
@@ -0,0 +1,10 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+{-# LANGUAGE KindSignatures, DataKinds #-}
+
+module Language.Haskell.Liquid.FinField where
+
+import GHC.TypeLits
+
+newtype FFld (o :: Nat) = FFld { ffToInteger :: Integer } deriving Eq
+
+-- see /tests/pos/FF17.hs and /tests/pos/FF2131.hs for usage examples
diff --git a/src/Language/Haskell/Liquid/FinField/FF17.hs b/src/Language/Haskell/Liquid/FinField/FF17.hs
new file mode 100644
--- /dev/null
+++ b/src/Language/Haskell/Liquid/FinField/FF17.hs
@@ -0,0 +1,26 @@
+{-# LANGUAGE DataKinds #-}
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+{-@ LIQUID "--smtsolver=cvc5"  @-}
+
+module Language.Haskell.Liquid.FinField.FF17 where
+
+import Language.Haskell.Liquid.FinField
+
+-- instantiate FFld for a specific prime value of 17
+data FF17 = FF17 { toFFld :: FFld 17 }
+{-@ embed FF17 as (FFld_t 17) @-}
+
+{-@ assume val :: n : Integer -> {v:FF17 | v = FF_val n} @-}
+{-@ define val    n                          = (FF_val n) @-}
+val :: Integer -> FF17
+val n = FF17 (FFld (n `mod` 17))
+
+{-@ assume add :: x : FF17 -> y : FF17 -> {v:FF17 | v = FF_add x y} @-}
+{-@ define add    x           y                      = (FF_add x y) @-}
+add :: FF17 -> FF17 -> FF17
+add x y = FF17 (FFld (ffToInteger (toFFld x) + ffToInteger (toFFld y) `mod` 17))
+
+{-@ assume mul :: x : FF17 -> y : FF17 -> {v:FF17 | v = FF_mul x y} @-}
+{-@ define mul    x           y                      = (FF_mul x y) @-}
+mul :: FF17 -> FF17 -> FF17
+mul x y = FF17 (FFld (ffToInteger (toFFld x) * ffToInteger (toFFld y) `mod` 17))