diff --git a/DifferenceLogic.cabal b/DifferenceLogic.cabal
--- a/DifferenceLogic.cabal
+++ b/DifferenceLogic.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                DifferenceLogic
-version:             0.1.0.2
+version:             0.1.0.4
 synopsis:            A theory solver for conjunctions of literals in difference logic
 description:         This package contains a theory solver for conjunctions of literals
 		     in difference logic. The logic supports predicates:
diff --git a/src/DifferenceLogic/Solver.hs b/src/DifferenceLogic/Solver.hs
--- a/src/DifferenceLogic/Solver.hs
+++ b/src/DifferenceLogic/Solver.hs
@@ -1,6 +1,7 @@
 module DifferenceLogic.Solver(
-  ZFormula, ZLiteral,
+  IntegerDifferenceLogic,
   integerDifferenceLogic,
+  ZFormula, ZLiteral,
   zF,
   zLit,
   eq, gt, lt, geq, leq,
@@ -29,7 +30,7 @@
   functions t = S.singleton minusFunc
   decideSat t lits = case decideSatisfiability $ zF $ S.toList $ S.map toZLiteral lits of
     True -> (True, S.empty)
-    False -> (False, lits)
+    False -> (False, S.map negateLit lits)
 
 minusFunc = functionDecl "-" 2 [U.sort "Integer", U.sort "Integer"] (U.sort "Integer")