diff --git a/app/Checked/X1.hs b/app/Checked/X1.hs
new file mode 100644
--- /dev/null
+++ b/app/Checked/X1.hs
@@ -0,0 +1,3 @@
+module Checked.X1 (x) where
+
+import Checked.X2
diff --git a/app/Checked/X2.hs b/app/Checked/X2.hs
new file mode 100644
--- /dev/null
+++ b/app/Checked/X2.hs
@@ -0,0 +1,5 @@
+module Checked.X2 where
+
+{-@ x :: {v:Int | v = 2} @-}
+x :: Int
+x = 2
diff --git a/app/FFI.hs b/app/FFI.hs
--- a/app/FFI.hs
+++ b/app/FFI.hs
@@ -1,5 +1,7 @@
 import Foreign.C.Types
 
+import Unchecked
+
 {-@ embed CInt as int @-}
 {-@ embed Integer as int @-}
 
@@ -8,7 +10,7 @@
   :: CInt -> IO CInt
 
 main :: IO ()
-main = print =<< foo 1
+main = print =<< foo x
 
 {-@ foo :: x:{Int | x > 0} -> IO Int @-}
 foo :: Int -> IO Int
diff --git a/app/Unchecked.hs b/app/Unchecked.hs
new file mode 100644
--- /dev/null
+++ b/app/Unchecked.hs
@@ -0,0 +1,7 @@
+module Unchecked where
+
+import qualified Checked.X1
+
+{-@ x :: {v:Int | v = 1} @-}
+x :: Int
+x = Checked.X1.x -- == 2
diff --git a/liquidhaskell-cabal-demo.cabal b/liquidhaskell-cabal-demo.cabal
--- a/liquidhaskell-cabal-demo.cabal
+++ b/liquidhaskell-cabal-demo.cabal
@@ -1,8 +1,8 @@
 name:                     liquidhaskell-cabal-demo
-version:                  0.2.0.1
+version:                  0.2.1.0
 synopsis:                 Demo of Liquid Haskell integration for Cabal and stack
 description:              Please see the
-                          <https://github.com/spinda/liquidhaskell-cabal-demo/blob/0.2.0.1/README.md README>
+                          <https://github.com/spinda/liquidhaskell-cabal-demo/blob/0.2.1.0/README.md README>
                           on GitHub for more information.
 homepage:                 https://github.com/spinda/liquidhaskell-cabal-demo#readme
 bug-reports:              https://github.com/spinda/liquidhaskell-cabal-demo/issues
@@ -17,7 +17,7 @@
 extra-source-files:       include/foo.h
 
 custom-setup
-  setup-depends:           base, Cabal, liquidhaskell-cabal >= 0.2.0
+  setup-depends:           base, Cabal, liquidhaskell-cabal >= 0.2.1
 
 flag liquidhaskell
   description:             After building, verify with LiquidHaskell
@@ -26,7 +26,7 @@
 library
   exposed-modules:         A, B, C
   build-depends:           base >=4.8 && <5
-                         , liquidhaskell-cabal >= 0.2
+                         , liquidhaskell-cabal >= 0.2.1
   hs-source-dirs:          src
   default-language:        Haskell2010
   default-extensions:      TupleSections
@@ -35,8 +35,11 @@
 
 executable ffi
   main-is:                 FFI.hs
+  other-modules:           Checked.X1
+                         , Checked.X2
+                         , Unchecked
   build-depends:           base >=4.8 && <5
-                         , liquidhaskell-cabal >= 0.2
+                         , liquidhaskell-cabal >= 0.2.1
   hs-source-dirs:          app
   default-language:        Haskell2010
   default-extensions:      ForeignFunctionInterface
@@ -47,6 +50,9 @@
                            -with-rtsopts=-N
                            -Wall
   x-liquidhaskell-options: --diff
+  x-liquidhaskell-options: --no-termination
+  x-liquidhaskell-verify: app/FFI.hs
+  x-liquidhaskell-verify: app/Checked
 
 source-repository head
   type:                git