Small rewrite

        let k = makeVar n

        in  (Equation lhs Eq (rhs :+: ((Const m) :*: (Var k))), [k])

eliminateModulo' n makeVar (Equation lhs (ModNe m) rhs) =

        let j = makeVar (n + 1)

            k = makeVar n

        let j = makeVar n

            k = makeVar (n + 1)

        in  ((Equation lhs Eq (rhs :+: ((Var j) :+: ((Const m) :*: (Var k))))) :&:

            (Equation (Const 0) Lt (Var j)) :&: (Equation (Var j) Lt (Const m)), [k, j])

            (Equation (Const 0) Lt (Var j)) :&: (Equation (Var j) Lt (Const m)), [j, k])

eliminateModulo' n makeVar (g :|: h) =

        let (g', ag) = eliminateModulo' n makeVar g

            (h', ah) = eliminateModulo' (n + length ag) makeVar h

opToFunction Ne = (./=)

opToFunction Le = (.<=)

opToFunction Lt = (.<)

opToFunction (ModEq _) = error "symbolic modulo not supported"

opToFunction (ModNe _) = error "symbolic modulo not supported"

evaluateFormula :: (Ord a, Show a) => Formula a -> SIMap a -> SBool

evaluateFormula FTrue _ = true