diff --git a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
index cec6feb02dcfd8c54c27a7b702978362b0327dca..061e8924065a7830032d00bd69035d4a4933b15c 100644
--- a/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
+++ b/examples/javawlp_edsl/src/nl/uu/javawlp_edsl/Main.java
@@ -29,6 +29,18 @@ public class Main {
         pre(~(a * 2) == (79 & 40)); // can't evaluate due to undefined variable
     }
 
+    public static float float1(float a) {
+        pre(a >= 2);
+        a += a;
+        post(a >= 4);
+    }
+
+    public static float float2(float a) {
+        pre(a > 2 || a == 2);
+        a = a * 2;
+        post(a > 4 || a == 4);
+    }
+
     public static int mymin(int[] a, int b) {
         assert forall(a, i -> {
             return a[i] > b;
diff --git a/javawlp.cabal b/javawlp.cabal
index c6f00f207407797a4954d609a871bbfcfd5c1a4e..14b91a88731ff15a14d12d5c2f4375438188dfef 100644
--- a/javawlp.cabal
+++ b/javawlp.cabal
@@ -26,7 +26,6 @@ library
                      , LogicIR.Backend.Z3
                      , LogicIR.Backend.Test
                      , LogicIR.Backend.ModelGenerator
-                     , LogicIR.Backend.SBV
                      , LogicIR.Backend.Pretty
                      , LogicIR.Backend.Null
                      , LogicIR.Fold
@@ -50,7 +49,6 @@ library
                      , pretty
                      , mtl
                      , containers
-                     , sbv
   default-language:    Haskell2010
 
 test-suite javawlp-tests
diff --git a/src/LogicIR/Backend/Pretty.hs b/src/LogicIR/Backend/Pretty.hs
index a311066cdd4a737dbfbd42c47d1ea853076fac75..4af16c1d5a43ec251dfab5521830e8db84aa88b4 100644
--- a/src/LogicIR/Backend/Pretty.hs
+++ b/src/LogicIR/Backend/Pretty.hs
@@ -13,6 +13,7 @@ prettyLExpr = foldLExpr prettyLExprAlgebra
 prettyType :: Type -> String
 prettyType (TPrim PInt32) = "int"
 prettyType (TPrim PBool)  = "bool"
+prettyType (TPrim PFloat)  = "float"
 prettyType (TArray t)     = prettyType t ++ "[]"
 
 prettyLBinop :: LBinop -> String
@@ -43,7 +44,7 @@ prettyNUnop op =
     LNot -> "!"
 
 prettyVar :: Var -> String
-prettyVar (Var t n) = prettyType t ++ ":" ++ n
+prettyVar (Var t n) = n ++ ":" ++ prettyType t
 
 prettyLExprAlgebra :: LExprAlgebra String
 prettyLExprAlgebra = (fConst, prettyVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) where
diff --git a/src/LogicIR/Backend/Z3.hs b/src/LogicIR/Backend/Z3.hs
index e45d099d1053fdc816e290f86613154de08ee65c..6b1977f433895ee67b0be4d2aef935e7a2156143 100644
--- a/src/LogicIR/Backend/Z3.hs
+++ b/src/LogicIR/Backend/Z3.hs
@@ -16,12 +16,14 @@ lExprToZ3AstAlgebra = (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull
     fConst c = case c of
       CBool b -> mkBool b
       CInt n -> mkBitvector 32 (fromIntegral n)
+      CFloat f -> mkRealNum f
       CNil -> error "null constants cannot be used directly with Z3 (use LogicIR.Backend.Null)"
     fVar (Var t n) = do
       symbol <- mkStringSymbol n
       case t of
         "int" -> mkBvVar symbol 32
         "bool" -> mkBoolVar symbol
+        "float" -> mkRealVar symbol
         "[int]" -> do
           intSort <- mkBvSort 32
           arraySort <- mkArraySort intSort intSort
diff --git a/src/LogicIR/Expr.hs b/src/LogicIR/Expr.hs
index 7049765340894e095715ef17e607c20099d06f0b..e9160a54d2717eab97d6204506350845e49aa394 100644
--- a/src/LogicIR/Expr.hs
+++ b/src/LogicIR/Expr.hs
@@ -5,6 +5,7 @@ import Data.String
 -- | The primitive types are bool and int32.
 data Primitive = PBool
                | PInt32
+               | PFloat
                deriving (Show, Eq, Read)
 
 -- | A Type can either be a primitive or an array type.
@@ -52,6 +53,7 @@ data QOp = QAll | QAny
 -- | Constants.
 data LConst = CBool Bool
             | CInt Int
+            | CFloat Float
             | CNil
             deriving (Show, Eq, Read)
 
diff --git a/src/LogicIR/Fold.hs b/src/LogicIR/Fold.hs
index 28567887f442e4a53a767bad1c2336979f9420b5..dbed0f9c19b14fdc67a0ca82c0cb3c5ee1714c9c 100644
--- a/src/LogicIR/Fold.hs
+++ b/src/LogicIR/Fold.hs
@@ -15,6 +15,7 @@ type LExprAlgebra r = (LConst -> r, -- LConst
                       )
 
 -- Fold for logical expressions
+foldLExpr :: LExprAlgebra r -> LExpr -> r 
 foldLExpr (fConst, fVar, fUnop, fBinop, fIf, fQuant, fArray, fIsnull, fLen) = fold where
     fold e = case e of
                   LConst c       -> fConst c
diff --git a/src/LogicIR/Frontend/Java.hs b/src/LogicIR/Frontend/Java.hs
index 5f80a7c2e6efb771ebdb7342896096b62c088669..4debba0c60f49e05c958cac4cc6c5deabaaca69d 100644
--- a/src/LogicIR/Frontend/Java.hs
+++ b/src/LogicIR/Frontend/Java.hs
@@ -23,6 +23,7 @@ nameToVar name env decls =
     case arrayType of
         PrimType BooleanT                   -> fromString(symbol ++ ":bool")
         PrimType IntT                       -> fromString(symbol ++ ":int")
+        PrimType FloatT                     -> fromString(symbol ++ ":float")
         RefType (ArrayType (PrimType IntT)) -> fromString(symbol ++ ":[int]")
         _ -> error $ "Unimplemented nameToVar: " ++ show (name, arrayType)
     where
diff --git a/src/LogicIR/Parser.hs b/src/LogicIR/Parser.hs
index feeeb720e642c8d063384c44ee04cab310280efa..ce5c222b0211f94982772ebb109885a5b385c30c 100644
--- a/src/LogicIR/Parser.hs
+++ b/src/LogicIR/Parser.hs
@@ -92,7 +92,9 @@ bvarP = do
 typeP :: Parser Type
 typeP = try (TPrim <$> primTypeP) <|> (TArray <$> arrayTypeP)
   where
-    primTypeP = lexeme $ (PBool <$ str "bool") <|> (PInt32 <$ str "int")
+    primTypeP = lexeme (PBool <$ str "bool")
+                   <|> (PInt32 <$ str "int")
+                   <|> (PFloat <$ str "float")
     arrayTypeP = "[" ~> typeP <~ "]"
 
 -- | Useful marcros.
diff --git a/stack.yaml b/stack.yaml
index 5307da20aa8ee88d3d9f80d4219fbe2929cfb849..2dfeca2b41ed909f724df038ac86040e3583d32d 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -49,9 +49,6 @@ packages:
 # (e.g., acme-missiles-0.3)
 extra-deps:
 - z3-4.1.2
-- sbv-7.4
-- crackNum-1.9
-- FloatingHex-0.4
 
 # Override default flag values for local packages and extra-deps
 # flags: {}