diff --git a/.circleci/config.yml b/.circleci/config.yml
index 4d8688b861..217119bbe7 100644
--- a/.circleci/config.yml
+++ b/.circleci/config.yml
@@ -27,7 +27,7 @@ commands:
       - checkout
       - add_ssh_keys
       - run: git submodule sync
-      - run: git submodule update --init
+      - run: git submodule update --init --remote
 
   cabal_build_and_test:
     description: "Build the project and run the tests"
diff --git a/.gitmodules b/.gitmodules
index 69a285528e..540cd3ece5 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +1,4 @@
 [submodule "liquid-fixpoint"]
 	path = liquid-fixpoint
-	url = https://github.com/ucsd-progsys/liquid-fixpoint.git
\ No newline at end of file
+	url = https://github.com/clayrat/liquid-fixpoint.git
+	branch = finfield
\ No newline at end of file
diff --git a/liquid-prelude/liquid-prelude.cabal b/liquid-prelude/liquid-prelude.cabal
index bef5ba0859..e55671d727 100644
--- a/liquid-prelude/liquid-prelude.cabal
+++ b/liquid-prelude/liquid-prelude.cabal
@@ -25,6 +25,7 @@ library
                     Language.Haskell.Liquid.Equational
                     Language.Haskell.Liquid.Bag
                     Language.Haskell.Liquid.ProofCombinators
+                    Language.Haskell.Liquid.FinField
   hs-source-dirs:     src
   build-depends:      base          < 5
                     , ghc-prim
diff --git a/liquid-prelude/src/Language/Haskell/Liquid/FinField.hs b/liquid-prelude/src/Language/Haskell/Liquid/FinField.hs
new file mode 100644
index 0000000000..1b4c81b436
--- /dev/null
+++ b/liquid-prelude/src/Language/Haskell/Liquid/FinField.hs
@@ -0,0 +1,32 @@
+{-# OPTIONS_GHC -fplugin=LiquidHaskell #-}
+{-# LANGUAGE KindSignatures, DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+module Language.Haskell.Liquid.FinField where
+
+import Data.Proxy
+import GHC.TypeLits
+import Language.Haskell.Liquid.Prelude
+
+data FFld (o :: Nat) = FFld { ffToInteger :: Integer } deriving Eq
+{-@ embed FFld as FFld_t @-}
+
+{-@ assume val :: forall o. KnownNat o => o : Nat -> n : Integer -> {v:FFld o | v = FF_val n} @-}
+{-@ define val                            o          n                           = (FF_val n) @-}
+val :: Int -> Integer -> FFld o
+val _ n = FFld n
+
+{-@ assume add :: forall o. KnownNat o => x : FFld o -> y : FFld o -> {v:FFld o | v = FF_add x y} @-}
+{-@ define add                            x             y                          = (FF_add x y) @-}
+add :: forall o. KnownNat o => FFld o -> FFld o -> FFld o
+add x y =
+  FFld (ffToInteger x + ffToInteger y `mod` liquidAssume (n /= 0) n)
+  where
+  n = natVal (Proxy :: Proxy o)
+
+{-@ assume mul :: forall o. KnownNat o => x : FFld o -> y : FFld o -> {v:FFld o | v = FF_mul x y} @-}
+{-@ define mul                            x             y                          = (FF_mul x y) @-}
+mul :: forall o. KnownNat o => FFld o -> FFld o -> FFld o
+mul x y = FFld (ffToInteger x * ffToInteger y `mod` liquidAssume (n /= 0) n)
+  where
+  n = natVal (Proxy :: Proxy o)
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Elaborate.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Elaborate.hs
index 367f7a0308..6dab96eee1 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Elaborate.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/Bare/Elaborate.hs
@@ -556,6 +556,7 @@ renameBinderSort f = rename
   rename F.FInt             = F.FInt
   rename F.FReal            = F.FReal
   rename F.FNum             = F.FNum
+  rename (F.FNatNum n)      = F.FNatNum n
   rename F.FFrac            = F.FFrac
   rename (   F.FObj s     ) = F.FObj (f s)
   rename t'@(F.FVar _     ) = t'
diff --git a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
index 60084ea7e8..70b00e7173 100644
--- a/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
+++ b/liquidhaskell-boot/src/Language/Haskell/Liquid/WiredIn.hs
@@ -95,7 +95,7 @@ wiredTheorySortedSyms =
     | s <- wiredTheorySyms
     , let srt = F.tsSort $
                   fromMaybe (panic Nothing ("unknown symbol: " ++ show s)) $
-                    F.lookupSEnv s (F.theorySymbols F.Z3)
+                    F.lookupSEnv s (F.theorySymbols F.Z3 <> F.theorySymbols F.Cvc5)
     ]
   where
     wiredTheorySyms =
@@ -122,6 +122,10 @@ wiredTheorySortedSyms =
       , "Bag_union"
       , "Bag_union_max"
 
+      , "FF_val"
+      , "FF_add"
+      , "FF_mul"
+
       , "strLen"
       ]