type verification

4 files changed, 369 insertions, 43 deletions

diff --git a/src/theory/rewriter/compiler.py b/src/theory/rewriter/compiler.py
index ebf3b9d84..c69cf7d08 100755
--- a/src/theory/rewriter/compiler.py
+++ b/src/theory/rewriter/compiler.py
@@ -12,6 +12,8 @@ from parser import parse_rules
 
 from backend_lfsc import collect_params
 
+import smt_switch as ss
+
 op_to_kind = {
     Op.BVUGT: "BITVECTOR_UGT",
     Op.BVUGE: "BITVECTOR_UGE",
@@ -75,6 +77,7 @@ op_to_const_eval = {
     Op.PLUS: lambda args: "({} + {})".format(args[0], args[1]),
     Op.MINUS: lambda args: "({} - {})".format(args[0], args[1]),
     Op.MULT: lambda args: "({} * {})".format(args[0], args[1]),
+    Op.MOD: lambda args: "({} % {})".format(args[0], args[1]),
     Op.LEQ: lambda args: "({} <= {})".format(args[0], args[1]),
     Op.LT: lambda args: "({} < {})".format(args[0], args[1]),
     Op.GEQ: lambda args: "({} >= {})".format(args[0], args[1]),
@@ -670,8 +673,16 @@ def expr_to_code(expr):
         elif expr.op == Op.BV_VAL:
             return f"({args[0]}).getValue()"
         elif expr.op == Op.BVCONST:
-            val = f"Integer({args[0]})" if expr.children[0].sort.base == BaseSort.Int32 else args[0]
-            width = f"{args[1]}.getUnsignedInt()" if expr.children[1].sort.base == BaseSort.Int else args[1]
+            val = (
+                f"Integer({args[0]})"
+                if expr.children[0].sort.base == BaseSort.Int32
+                else args[0]
+            )
+            width = (
+                f"{args[1]}.getUnsignedInt()"
+                if expr.children[1].sort.base == BaseSort.Int
+                else args[1]
+            )
             return f"BitVector({width}, {val})"
         elif expr.op == Op.GET_CONST:
             sort = expr.children[0].sort
@@ -713,7 +724,10 @@ def expr_to_code(expr):
             if op_to_nindex[kind] != 0:
                 # Convert Integer to uint32_t for indices
                 for i, arg in enumerate(args[: op_to_nindex[kind] + 1]):
-                    if expr.children[i].sort and expr.children[i].sort.base == BaseSort.Int:
+                    if (
+                        expr.children[i].sort
+                        and expr.children[i].sort.base == BaseSort.Int
+                    ):
                         args[i] = f"{arg}.getUnsignedInt()"
 
                 op = "bv::utils::mkIndexedOp({})".format(
@@ -745,7 +759,10 @@ def expr_to_code(expr):
         elif expr.sort and expr.sort.const:
             if expr.sort.base == BaseSort.Int:
                 for i, arg in enumerate(args):
-                    if expr.children[i].sort and expr.children[i].sort.base == BaseSort.Int32:
+                    if (
+                        expr.children[i].sort
+                        and expr.children[i].sort.base == BaseSort.Int32
+                    ):
                         args[i] = f"Integer({arg})"
             return op_to_const_eval[expr.op](args)
         elif expr.op == Op.MAP:
@@ -1073,7 +1090,9 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
                         last = last and (not has_non_remainder)
                         curr_block = match_instrs
 
-                        if expr.op in nary_ops and len(nlist_children) == len(expr.children):
+                        if expr.op in nary_ops and len(nlist_children) == len(
+                            expr.children
+                        ):
                             curr_block.append(
                                 Assert(
                                     Fn(
@@ -1177,14 +1196,16 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
                                     Assign(child, Fn(Op.SLICE, [node, next_idx, var_i]))
                                 )
 
-                                if Op.CONCAT and isinstance(child.sort.children[0].children[0], Var):
+                                if Op.CONCAT and isinstance(
+                                    child.sort.children[0].children[0], Var
+                                ):
                                     len_var = child.sort.children[0].children[0]
-                                    list_node = Fn(Op.MK_NODE, [KindConst(Op.CONCAT), child])
+                                    list_node = Fn(
+                                        Op.MK_NODE, [KindConst(Op.CONCAT), child]
+                                    )
                                     list_node.sort = Sort(BaseSort.BitVec, [len_var])
                                     list_len = Fn(Op.BV_SIZE, [list_node])
-                                    loop_body.append(
-                                        Assign(len_var, list_len)
-                                    )
+                                    loop_body.append(Assign(len_var, list_len))
 
                                 max_val = mk_node(
                                     Op.PLUS,
@@ -1228,14 +1249,19 @@ def rule_to_match_ir(cfg, out_block, node_var, out_var, lhs):
 
                                     # TODO: merge with other case
                                     remainder = expr.children[-1]
-                                    if Op.CONCAT and isinstance(remainder.sort.children[0].children[0], Var):
+                                    if Op.CONCAT and isinstance(
+                                        remainder.sort.children[0].children[0], Var
+                                    ):
                                         len_var = remainder.sort.children[0].children[0]
-                                        list_node = Fn(Op.MK_NODE, [KindConst(Op.CONCAT), remainder])
-                                        list_node.sort = Sort(BaseSort.BitVec, [len_var])
-                                        list_len = Fn(Op.BV_SIZE, [list_node])
-                                        curr_block.append(
-                                            Assign(len_var, list_len)
+                                        list_node = Fn(
+                                            Op.MK_NODE,
+                                            [KindConst(Op.CONCAT), remainder],
+                                        )
+                                        list_node.sort = Sort(
+                                            BaseSort.BitVec, [len_var]
                                         )
+                                        list_len = Fn(Op.BV_SIZE, [list_node])
+                                        curr_block.append(Assign(len_var, list_len))
                                 expr_to_ir(
                                     child,
                                     loop_var,
@@ -1660,6 +1686,283 @@ def rule_to_lfsc(rule):
     print(rule_pattern.format(rule_name, "\n".join(varargs), lhs, rhs, closing_parens))
 
 
+def term_from_node(solver, context, expr, extra_cond):
+    if expr in context:
+        return context[expr]
+
+    if isinstance(expr, Var):
+        if expr not in context:
+            if expr.sort and expr.sort.is_int():
+                intsort = solver.make_sort(ss.sortkinds.INT)
+                context[expr] = solver.make_symbol(expr.name, intsort)
+            else:
+                print(f"Unsupported sort for {expr}: {expr.sort}")
+                assert False
+        return context[expr]
+    elif isinstance(expr, Fn):
+        if expr.sort.base == BaseSort.Bool and expr.children[0].sort.base == BaseSort.BitVec:
+            boolsort = solver.make_sort(ss.sortkinds.BOOL)
+            return solver.make_symbol(fresh_name("bv_pred"), boolsort)
+        elif expr.op == Op.POW2:
+            bw = term_from_node(solver, context, expr.children[0].sort.children[0], extra_cond)
+            intsort = solver.make_sort(ss.sortkinds.INT)
+            zero = solver.make_term(0, intsort)
+            context[expr] = solver.make_symbol(fresh_name("pow2"), intsort)
+            extra_cond.add(solver.make_term(ss.primops.Ge, context[expr], zero))
+            extra_cond.add(solver.make_term(ss.primops.Le, context[expr], bw))
+            return context[expr]
+        elif expr.op == Op.NPOW2:
+            bw = term_from_node(solver, context, expr.children[0].sort.children[0], extra_cond)
+            intsort = solver.make_sort(ss.sortkinds.INT)
+            zero = solver.make_term(0, intsort)
+            context[expr] = solver.make_symbol(fresh_name("npow2"), intsort)
+            extra_cond.add(solver.make_term(ss.primops.Ge, context[expr], zero))
+            extra_cond.add(solver.make_term(ss.primops.Le, context[expr], bw))
+            return context[expr]
+        elif expr.op == Op.ZEROES:
+            bw = term_from_node(solver, context, expr.children[0].sort.children[0], extra_cond)
+            intsort = solver.make_sort(ss.sortkinds.INT)
+            zero = solver.make_term(0, intsort)
+            context[expr] = solver.make_symbol(fresh_name("zeroes"), intsort)
+            extra_cond.add(solver.make_term(ss.primops.Ge, context[expr], zero))
+            extra_cond.add(solver.make_term(ss.primops.Le, context[expr], bw))
+            return context[expr]
+
+        terms = []
+        for child in expr.children:
+            terms.append(term_from_node(solver, context, child, extra_cond))
+
+        if expr.op == Op.PLUS:
+            return solver.make_term(ss.primops.Plus, *terms)
+        elif expr.op == Op.MINUS:
+            return solver.make_term(ss.primops.Minus, *terms)
+        elif expr.op == Op.EQ:
+            return solver.make_term(ss.primops.Equal, *terms)
+        elif expr.op == Op.LT:
+            return solver.make_term(ss.primops.Lt, *terms)
+        elif expr.op == Op.LEQ:
+            return solver.make_term(ss.primops.Le, *terms)
+        elif expr.op == Op.GEQ:
+            return solver.make_term(ss.primops.Ge, *terms)
+        elif expr.op == Op.AND:
+            return solver.make_term(ss.primops.And, *terms)
+        elif expr.op == Op.OR:
+            return solver.make_term(ss.primops.Or, *terms)
+        elif expr.op == Op.NOT:
+            return solver.make_term(ss.primops.Not, *terms)
+        elif expr.op == Op.MULT:
+            return solver.make_term(ss.primops.Mult, *terms)
+        elif expr.op == Op.MOD:
+            return solver.make_term(ss.primops.Mod, *terms)
+
+        print(f"Op not supported {expr.op}")
+        assert False
+    elif isinstance(expr, IntConst):
+        intsort = solver.make_sort(ss.sortkinds.INT)
+        return solver.make_term(expr.val, intsort)
+    elif isinstance(expr, BoolConst):
+        return solver.make_term(expr.val)
+    else:
+        print(f"Expr not supported {expr}")
+        assert False
+
+
+def get_type_invariants(lhs, solver, context, path_cond, expr, invariants, extra_cond):
+    def add_invariant(inv):
+        invariants.add(solver.make_term(ss.primops.Implies, path_cond, inv))
+
+    if isinstance(expr, Fn):
+        if expr.op == Op.COND:
+            not_prev_case_conds = solver.make_term(True)
+
+            bw = None
+            if expr.sort.base == BaseSort.BitVec:
+                bw = term_from_node(solver, context, expr.sort.children[0], extra_cond)
+
+            for case in expr.children:
+                case_cond = term_from_node(solver, context, case.children[0], extra_cond)
+                get_type_invariants(
+                    lhs,
+                    solver,
+                    context,
+                    path_cond,
+                    case.children[0],
+                    invariants,
+                    extra_cond,
+                )
+
+                cond = solver.make_term(ss.primops.And, not_prev_case_conds, case_cond)
+                not_prev_case_conds = solver.make_term(
+                    ss.primops.And,
+                    not_prev_case_conds,
+                    solver.make_term(ss.primops.Not, case_cond),
+                )
+                new_path_cond = solver.make_term(ss.primops.And, path_cond, cond)
+                get_type_invariants(
+                    lhs,
+                    solver,
+                    context,
+                    new_path_cond,
+                    case.children[1],
+                    invariants,
+                    extra_cond,
+                )
+
+                if bw is not None and case.children[1].sort.base != BaseSort.Fail:
+                    case_bw = term_from_node(
+                        solver, context, case.children[1].sort.children[0], extra_cond
+                    )
+                    inv = solver.make_term(ss.primops.Equal, case_bw, bw)
+                    extra_cond.add(solver.make_term(ss.primops.Implies, new_path_cond, inv))
+
+                if isinstance(case.children[1], Fn) and case.children[1].op == Op.FAIL:
+                    # Assert that we don't take fail paths
+                    extra_cond.add(solver.make_term(ss.primops.Not, cond))
+        elif expr.op == Op.LET:
+            if expr.children[1].sort.is_int():
+                context[expr.children[0]] = term_from_node(
+                    solver, context, expr.children[1], extra_cond
+                )
+            get_type_invariants(
+                lhs, solver, context, path_cond, expr.children[2], invariants, extra_cond
+            )
+        elif expr.op == Op.MAP:
+            lambda_context = dict(context)
+            get_type_invariants(
+                lhs, solver, lambda_context, path_cond, expr.children[0].children[1], invariants, extra_cond
+            )
+        elif expr.op == Op.BVCONST:
+            intsort = solver.make_sort(ss.sortkinds.INT)
+            zero = solver.make_term(0, intsort)
+            val = term_from_node(solver, context, expr.children[0], extra_cond)
+            add_invariant(solver.make_term(ss.primops.Ge, val, zero))
+        else:
+            for child in expr.children:
+                get_type_invariants(
+                    lhs, solver, context, path_cond, child, invariants, extra_cond
+                )
+
+            if expr.op == Op.EXTRACT:
+                intsort = solver.make_sort(ss.sortkinds.INT)
+                zero = solver.make_term(0, intsort)
+                high = term_from_node(solver, context, expr.children[0], extra_cond)
+                low = term_from_node(solver, context, expr.children[1], extra_cond)
+                inner_bw = term_from_node(
+                    solver, context, expr.children[2].sort.children[0], extra_cond
+                )
+                add_invariant(solver.make_term(ss.primops.Ge, high, zero))
+                add_invariant(solver.make_term(ss.primops.Ge, low, zero))
+                add_invariant(solver.make_term(ss.primops.Ge, high, low))
+                add_invariant(solver.make_term(ss.primops.Gt, inner_bw, high))
+            elif expr.op in [
+                Op.ROTATE_LEFT,
+                Op.ROTATE_RIGHT,
+                Op.SIGN_EXTEND,
+                Op.ZERO_EXTEND,
+            ]:
+                intsort = solver.make_sort(ss.sortkinds.INT)
+                zero = solver.make_term(0, intsort)
+                amount = term_from_node(solver, context, expr.children[0], extra_cond)
+                add_invariant(solver.make_term(ss.primops.Ge, amount, zero))
+            elif expr.op in [Op.BVULT, Op.BVADD, Op.BVAND, Op.BVOR, Op.BVXOR, Op.BVMUL, Op.BVSUB, Op.BVSHL] or (expr.op == Op.EQ and expr.children[0].sort.base == BaseSort.BitVec):
+                bw = None
+                for child in expr.children:
+                    child_bw = None
+                    if child.sort.base == BaseSort.List:
+                        child_bw = term_from_node(solver, context, child.sort.children[0].children[0], extra_cond)
+                    else:
+                        child_bw = term_from_node(solver, context, child.sort.children[0], extra_cond)
+
+                    if bw is None:
+                        bw = child_bw
+                    else:
+                        add_invariant(solver.make_term(ss.primops.Equal, bw, child_bw))
+            elif expr.op == Op.CONCAT:
+                lists = []
+                for child in expr.children:
+                    if child.sort.base == BaseSort.List:
+                        # Bit-widths of lists in concats are >= 0
+                        intsort = solver.make_sort(ss.sortkinds.INT)
+                        zero = solver.make_term(0, intsort)
+                        bw = term_from_node(
+                            solver, context, child.sort.children[0].children[0], extra_cond
+                        )
+                        add_invariant(solver.make_term(ss.primops.Ge, bw, zero))
+                        lists.append(child)
+
+                if lhs and len(lists) >= len(expr.children) - 1:
+                    # If there is at most one non-list item, then at least one
+                    # of the list items must be non-empty
+                    disj = []
+                    for l in lists:
+                        intsort = solver.make_sort(ss.sortkinds.INT)
+                        zero = solver.make_term(0, intsort)
+                        bw = term_from_node(
+                            solver, context, l.sort.children[0].children[0], extra_cond
+                        )
+                        disj.append(solver.make_term(ss.primops.Gt, bw, zero))
+                    add_invariant(solver.make_term(ss.primops.Or, disj))
+
+    if expr.sort and expr.sort.base == BaseSort.BitVec:
+        # Bit-widths are positive
+        intsort = solver.make_sort(ss.sortkinds.INT)
+        zero = solver.make_term(0, intsort)
+        bw = term_from_node(solver, context, expr.sort.children[0], extra_cond)
+        add_invariant(solver.make_term(ss.primops.Gt, bw, zero))
+
+
+def verify_types(rule):
+    solver = ss.solvers["cvc4"](False)
+    solver.set_opt("produce-models", "true")
+    solver.set_logic("QF_NIA")
+
+    context = dict()
+
+    preconds = set()
+    path_cond = solver.make_term(True)
+    get_type_invariants(True, solver, context, path_cond, rule.lhs, preconds, preconds)
+
+    postconds = set()
+    get_type_invariants(False, solver, context, path_cond, rule.rhs, postconds, preconds)
+
+    if rule.lhs.sort.base == BaseSort.BitVec and rule.rhs.sort.base == BaseSort.BitVec:
+        lhs_bw = term_from_node(solver, context, rule.lhs.sort.children[0], preconds)
+        rhs_bw = term_from_node(solver, context, rule.rhs.sort.children[0], preconds)
+        postconds.add(solver.make_term(ss.primops.Equal, lhs_bw, rhs_bw))
+        print(solver.make_term(ss.primops.Equal, lhs_bw, rhs_bw))
+
+    for precond in preconds:
+        print(f"PRECOND {precond}")
+        solver.assert_formula(precond)
+    for postcond in postconds:
+        print(f"POSTCOND {postcond}")
+
+    if not postconds:
+        print(f"WARNING: no type checks for {rule.name}")
+        return
+
+    # cond = solver.make_term(
+    #     ss.primops.Or,
+    #     [solver.make_term(ss.primops.Not, postcond) for postcond in postconds],
+    # )
+    for postcond in postconds:
+        solver.push()
+        solver.assert_formula(solver.make_term(ss.primops.Not, postcond))
+        r = solver.check_sat()
+        if not r.is_unsat():
+            print(f"{rule.name}: Type check failed. Condition: {postcond}")
+            for v, t in context.items():
+                print(f"{v.name} => {solver.get_value(t)}")
+            assert False
+        solver.pop()
+
+    print(f"{rule.name}: Type check successful")
+
+
+def verify_rule(rule):
+    verify_types(rule)
+
+
 def type_check(rules):
     for rule in rules:
         print(f"Type checking {rule.name}")
@@ -1687,6 +1990,14 @@ def dump_ir(args):
     print(gen_rules_implementation(rules))
 
 
+def verify(args):
+    rules = parse_rules(args.infile.read())
+    # rules = [rule for rule in rules if rule.name == args.rewrite]
+    type_check(rules)
+    for rule in rules:
+        verify_rule(rule)
+
+
 def main():
     parser = argparse.ArgumentParser(description="Compile rewrite rules.")
     subparsers = parser.add_subparsers()
@@ -1708,6 +2019,11 @@ def main():
     parser_dump_ir.add_argument("rewrite", help="Name of the rewrite to dump")
     parser_dump_ir.set_defaults(func=dump_ir)
 
+    parser_dump_ir = subparsers.add_parser("verify")
+    parser_dump_ir.add_argument("infile", type=argparse.FileType("r"), help="Rule file")
+    parser_dump_ir.add_argument("rewrite", help="Name of the rewrite to dump")
+    parser_dump_ir.set_defaults(func=verify)
+
     args = parser.parse_args()
     args.func(args)
 
diff --git a/src/theory/rewriter/node.py b/src/theory/rewriter/node.py
index 7c2187ee2..dce4b7408 100644
--- a/src/theory/rewriter/node.py
+++ b/src/theory/rewriter/node.py
@@ -83,6 +83,7 @@ class Op(Enum):
     LT = auto()
     GEQ = auto()
     LEFT_SHIFT = auto()
+    MOD = auto()
 
     ###########################################################################
     # Theory-independent
@@ -360,6 +361,8 @@ def infer_types(context, node):
     if isinstance(node, Var):
         # Variable sorts are declared in the context
         node.sort = context[node.name]
+        for child in node.sort.children:
+            infer_types(context, child)
         return
 
     if isinstance(node, Fn):
@@ -489,11 +492,14 @@ def infer_types(context, node):
                         node.children[1].sort.children[:])
         elif node.op in [Op.COND]:
             # TODO: check that types are the same across branches
-            sort = Sort(node.children[0].sort.base,
-                        node.children[0].sort.children[:])
+            if node.children[0].sort.base == BaseSort.BitVec:
+                sort = Sort(BaseSort.BitVec, [Var(fresh_name("bw"), Sort(BaseSort.Int32, [], True))])
+            else:
+                sort = Sort(node.children[0].sort.base,
+                            node.children[0].sort.children[:])
         elif node.op in [Op.BVCONST]:
             sort = Sort(BaseSort.BitVec, [node.children[1]])
-        elif node.op in [Op.PLUS, Op.MINUS, Op.MULT]:
+        elif node.op in [Op.PLUS, Op.MINUS, Op.MULT, Op.MOD]:
             assert node.children[0].sort.is_int()
             assert node.children[1].sort.is_int()
             sort = unify_int_sorts(node.children[0].sort, node.children[1].sort)
diff --git a/src/theory/rewriter/parser.py b/src/theory/rewriter/parser.py
index a6efacd03..9b9bf5c7b 100644
--- a/src/theory/rewriter/parser.py
+++ b/src/theory/rewriter/parser.py
@@ -49,6 +49,7 @@ symbol_to_op = {
     'xor': Op.XOR,
     '+': Op.PLUS,
     '-': Op.MINUS,
+    'mod': Op.MOD,
     '*': Op.MULT,
     '<': Op.LT,
     '>=': Op.GEQ,
diff --git a/src/theory/rewriter/rules/basic.rules b/src/theory/rewriter/rules/basic.rules
index 04fc09605..dd0233398 100644
--- a/src/theory/rewriter/rules/basic.rules
+++ b/src/theory/rewriter/rules/basic.rules
@@ -21,11 +21,11 @@
 
 /* ExtractConcat */
 
-(define-rule ExtractExtract ((i Int :const) (j Int :const) (k Int :const) (l Int :const) (x (_ BitVec n)))
+(define-rule ExtractExtract ((i Int :const) (j Int :const) (k Int :const) (l Int :const) (n Int :const) (x (_ BitVec n)))
   ((_ extract i j) ((_ extract k l) x))
   ((_ extract (+ i l) (+ j l)) x))
 
-(define-rule SimplifyEq ((x (_ BitVec n)))
+(define-rule SimplifyEq ((n Int :const) (x (_ BitVec n)))
   (= x x)
   true)
 
@@ -193,15 +193,17 @@
 
 (define-rule RotateLeftEliminate ((i Int :const) (n Int :const) (x (_ BitVec n)))
     ((_ rotate_left i) x)
-    (cond
-      ((= i 0) x)
-      (concat ((_ extract (- n (+ 1 i)) 0) x) ((_ extract (- n 1) (- n i)) x))))
+    (let ((a (mod i n)))
+      (cond
+        ((= a 0) x)
+        (concat ((_ extract (- n (+ 1 a)) 0) x) ((_ extract (- n 1) (- n a)) x)))))
 
 (define-rule RotateRightEliminate ((i Int :const) (n Int :const) (x (_ BitVec n)))
     ((_ rotate_right i) x)
-    (cond
-      ((= i 0) x)
-      (concat ((_ extract (- i 1) 0) x) ((_ extract (- n 1) i) x))))
+    (let ((a (mod i n)))
+      (cond
+        ((= a 0) x)
+        (concat ((_ extract (- a 1) 0) x) ((_ extract (- n 1) a) x)))))
 
 /* BVToNatEliminate: COMPLEX */
 
@@ -457,7 +459,7 @@
     (= ((_ extract (- n 1) (- n 1)) x) (_ bv 1 1)))
 
 /* Note: Duplicate of LtSelfUlt */
-(define-rule UltSelf ((x (_ BitVec n)))
+(define-rule UltSelf ((n Int :const) (x (_ BitVec n)))
     (bvult x x)
     false)
 
@@ -466,7 +468,7 @@
     (= x (_ bv 0 n)))
 
 /* Note: Duplicate of LteSelfUle */
-(define-rule UleSelf ((x (_ BitVec n)))
+(define-rule UleSelf ((n Int :const) (x (_ BitVec n)))
     (bvule x x)
     true)
 
@@ -474,7 +476,7 @@
     (bvule (_ bv 0 n) x)
     true)
 
-(define-rule NotUlt ((x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule NotUlt ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
     (not (bvult x y))
     (bvule y x))
 
@@ -482,7 +484,7 @@
     (bvult x (bvnot (_ bv 0 n)))
     true)
 
-(define-rule NotUle ((x (_ BitVec n)) (y (_ BitVec n)))
+(define-rule NotUle ((n Int :const) (x (_ BitVec n)) (y (_ BitVec n)))
     (not (bvule x y))
     (bvult y x))
 
@@ -517,15 +519,14 @@
       ((= 1 (pow2 c)) x)
       ((< 0 (pow2 c)) (concat (_ bv 0 (- (pow2 c) 1)) ((_ extract (- n 1) (- (pow2 c) 1)) x)))))
 
-/* TODO: make pow2 neg */
 (define-rule UdivPowXNeg ((n Int :const) (c (_ BitVec n) :const) (x (_ BitVec n)) (xs (_ BitVec n) :list))
     (bvudiv x c)
     (cond 
       ((and (< 1 n) (= 1 (npow2 c))) (bvneg x))
       ((= 1 (npow2 c)) (bvneg x))
-      ((and (< 1 n) (< 0 (pow2 c)))
+      ((and (< 1 n) (< 0 (npow2 c)))
         (bvneg (concat (_ bv 0 (- (npow2 c) 1)) ((_ extract (- n 1) (- (npow2 c) 1)) x))))
-      ((< 0 (pow2 c))
+      ((< 0 (npow2 c))
         (concat (_ bv 0 (- (npow2 c) 1)) ((_ extract (- n 1) (- (npow2 c) 1)) x)))))
 
 (define-rule UdivZero ((n Int :const) (x (_ BitVec n)))
@@ -575,18 +576,20 @@
 
 (define-rule ZeroExtendEqConst ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
   (= ((_ zero_extend m) x) c)
-  (cond
-    ((= ((_ extract (- (+ n m) 1) n) c) (_ bv 0 m)) false)
-    (= x ((_ extract (- n 1) 0) c))))
+  (cond ((< 0 m)
+    (cond
+      ((= ((_ extract (- (+ n m) 1) n) c) (_ bv 0 m)) false)
+      (= x ((_ extract (- n 1) 0) c))))))
 
 (define-rule SignExtendEqConst ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
   (= ((_ sign_extend m) x) c)
-  (cond
-    ((or
-      (and (= ((_ extract (- n 1) (- n 1)) c) (_ bv 0 1)) (= ((_ extract (- (+ m n) 1) n) c) (_ bv 0 (- (+ n m) 1))))
-      (and (= ((_ extract (- n 1) (- n 1)) c) (_ bv 1 1)) (= ((_ extract (- (+ m n) 1) n) c) (bvnot (_ bv 0 (- (+ n m) 1))))))
-    (= x ((_ extract (- n 1) 0) c)))
-    false))
+  (cond ((< 0 m)
+    (cond
+      ((or
+        (and (= ((_ extract (- n 1) (- n 1)) c) (_ bv 0 1)) (= ((_ extract (- (+ m n) 1) (- n 1)) c) (_ bv 0 (+ m 1))))
+        (and (= ((_ extract (- n 1) (- n 1)) c) (_ bv 1 1)) (= ((_ extract (- (+ m n) 1) (- n 1)) c) (bvnot (_ bv 0 (+ m 1))))))
+      (= x ((_ extract (- n 1) 0) c)))
+      false))))
 
 (define-rule ZeroExtendUltConstLhs ((n Int :const) (m Int :const) (npm Int :const) (c (_ BitVec npm) :const) (x (_ BitVec n)))
   (bvult ((_ zero_extend m) x) c)