diff --git a/src/rules/add.rs b/src/rules/add.rs
index c55b561..582d436 100644
--- a/src/rules/add.rs
+++ b/src/rules/add.rs
@@ -10,8 +10,8 @@ pub fn add() -> Vec<Rewrite> {
         rw!("add-zero"      ; "(+ ?a 0)"                    => "?a"),
         rw!("add-dist-mul"  ; "(* ?a (+ ?b ?c))"            => "(+ (* ?a ?b) (* ?a ?c))"),
         rw!("add-fact-mul"  ; "(+ (* ?a ?b) (* ?a ?c))"     => "(* ?a (+ ?b ?c))"),
-        rw!("add-denom-mul" ; "(+ (/ ?a ?b) ?c)"            => "(/ (+ ?a (* ?b ?c)) ?b)"),
-        rw!("add-denom-div" ; "(/ (+ ?a (* ?b ?c)) ?b)"     => "(+ (/ ?a ?b) ?c)"),
+        rw!("add-denom-mul" ; "(+ (/ ?a ?b) ?c)"            => "(/ (+ ?a (* ?b ?c)) ?b)" if crate::trs::is_not_zero("?b")),
+        rw!("add-denom-div" ; "(/ (+ ?a (* ?b ?c)) ?b)"     => "(+ (/ ?a ?b) ?c)" if crate::trs::is_not_zero("?b")),
         rw!("add-div-mod"   ; "( + ( / ?x 2 ) ( % ?x 2 ) )" => "( / ( + ?x 1 ) 2 )"),
         //FOLD
         rw!("add-const"     ; "( + (* ?x ?a) (* ?y ?b))"    => "( * (+ (* ?x (/ ?a ?b)) ?y) ?b)" if crate::trs::compare_c0_c1("?a", "?b", "%0")),
diff --git a/src/rules/div.rs b/src/rules/div.rs
index d2938ee..27e6fec 100644
--- a/src/rules/div.rs
+++ b/src/rules/div.rs
@@ -5,14 +5,14 @@ pub type Rewrite = egg::Rewrite<Math, ConstantFold>;
 pub fn div() -> Vec<Rewrite> {
     vec![
         //DIV RULES
-        rw!("div-zero"      ; "(/ 0 ?x)"            => "(0)"),
+        rw!("div-zero"      ; "(/ 0 ?x)"            => "(0)" if crate::trs::is_not_zero("?x")),
         rw!("div-cancel"    ; "(/ ?a ?a)"           => "1" if crate::trs::is_not_zero("?a")),
-        rw!("div-minus-down"; "(/ (* -1 ?a) ?b)"    => "(/ ?a (* -1 ?b))"),
-        rw!("div-minus-up"  ; "(/ ?a (* -1 ?b))"    => "(/ (* -1 ?a) ?b)"),
-        rw!("div-minus-in"  ; "(* -1 (/ ?a ?b))"    => "(/ (* -1 ?a) ?b)"),
-        rw!("div-minus-out" ; "(/ (* -1 ?a) ?b)"    => "(* -1 (/ ?a ?b))"),
+        rw!("div-minus-down"; "(/ (* -1 ?a) ?b)"    => "(/ ?a (* -1 ?b))" if crate::trs::is_not_zero("?b")),
+        rw!("div-minus-up"  ; "(/ ?a (* -1 ?b))"    => "(/ (* -1 ?a) ?b)" if crate::trs::is_not_zero("?b")),
+        rw!("div-minus-in"  ; "(* -1 (/ ?a ?b))"    => "(/ (* -1 ?a) ?b)" if crate::trs::is_not_zero("?b")),
+        rw!("div-minus-out" ; "(/ (* -1 ?a) ?b)"    => "(* -1 (/ ?a ?b))" if crate::trs::is_not_zero("?b")),
         //FOLD
-        rw!("div-consts-div"; "( / ( * ?x ?a ) ?b )" => "( / ?x ( / ?b ?a ) )" if crate::trs::compare_c0_c1("?b", "?a", "%0<")),
+        rw!("div-consts-div"; "( / ( * ?x ?a ) ?b )" => "( / ?x ( / ?b ?a ) )" if crate::trs::compare_c0_c1("?b", "?a", "%0<0")),
         rw!("div-consts-mul"; "( / ( * ?x ?a ) ?b )" => "( * ?x ( / ?a ?b ) )" if crate::trs::compare_c0_c1("?a", "?b", "%0<")),
         rw!("div-consts-add"; "( / ( + ( * ?x ?a ) ?y ) ?b )" => "( + ( * ?x ( / ?a ?b ) ) ( / ?y ?b ) )" if crate::trs::compare_c0_c1("?a", "?b", "%0<")),
         rw!("div-separate"  ; "( / ( + ?x ?a ) ?b )" => "( + ( / ?x ?b ) ( / ?a ?b ) )" if crate::trs::compare_c0_c1("?a", "?b", "%0<")),
diff --git a/src/rules/lt.rs b/src/rules/lt.rs
index 600157f..f33f2ce 100644
--- a/src/rules/lt.rs
+++ b/src/rules/lt.rs
@@ -24,7 +24,7 @@ pub fn lt() -> Vec<Rewrite> {
         rw!("lt-min-max-cancel"     ; "(< (max ?a ?c) (min ?a ?b))"                 => "0"),
         // rw!("lt-mul-pos-cancel"     ; "(< (* ?x ?y) ?z)"                            => "(< ?x (/ ?z ?y))"  if crate::trs::is_const_pos("?y")),
         // rw!("lt-mul-div-cancel"     ; "(< ?x (/ ?z ?y))"                            => "(< (* ?x ?y) ?z))"  if crate::trs::is_const_pos("?y")),
-        rw!("lt-mul-pos-cancel"     ; "(< (* ?x ?y) ?z)"                            => "(< ?x ( / (- ( + ?z ?y ) 1 ) ?y ) ))"  if crate::trs::is_const_pos("?y")),
+        rw!("lt-mul-pos-cancel"     ; "(< (* ?x ?y) ?z)"                            => "(< ?x ( / (- ( + ?z ?y ) 1 ) ?y ) )"  if crate::trs::is_const_pos("?y")),
         rw!("lt-mul-div-cancel"     ; "(< ?y (/ ?x ?z))"                            => "( < ( - ( * ( + ?y 1 ) ?z ) 1 ) ?x )"  if crate::trs::is_const_pos("?z")),
         rw!("lt-const-mod"     ; "(< ?a (% ?x ?b))" => "1"  if crate::trs::compare_c0_c1("?a", "?b", "<=-a")),
         rw!("lt-const-mod-false"     ; "(< ?a (% ?x ?b))" => "0"  if crate::trs::compare_c0_c1("?a", "?b", ">=a")),
diff --git a/src/rules/modulo.rs b/src/rules/modulo.rs
index ba47ebb..d71c309 100644
--- a/src/rules/modulo.rs
+++ b/src/rules/modulo.rs
@@ -5,13 +5,13 @@ pub type Rewrite = egg::Rewrite<Math, ConstantFold>;
 pub fn modulo() -> Vec<Rewrite> {
     vec![
         //MOD RULES
-        rw!("mod-zero"      ; "(% 0 ?x)"             => "0"),
-        rw!("mod-x-x"       ; "(% ?x ?x)"            => "0"),
+        rw!("mod-zero"      ; "(% 0 ?x)"             => "0" if crate::trs::is_not_zero("?x")),
+        rw!("mod-x-x"       ; "(% ?x ?x)"            => "0" if crate::trs::is_not_zero("?x")),
         rw!("mod-one"       ; "(% ?x 1)"             => "0"),
         rw!("mod-const-add" ; "(% ?x ?c1)"           => "(% (+ ?x ?c1) ?c1)" if crate::trs::compare_c0_c1("?c1","?x","<=a")),
         rw!("mod-const-sub" ; "(% ?x ?c1)"           => "(% (- ?x ?c1) ?c1)" if crate::trs::compare_c0_c1("?c1","?x","<=a")),
-        rw!("mod-minus-out" ; "(% (* ?x -1) ?c)"     => "(* -1 (% ?x ?c))"),
-        rw!("mod-minus-in"  ; "(* -1 (% ?x ?c))"     => "(% (* ?x -1) ?c)"),
+        rw!("mod-minus-out" ; "(% (* ?x -1) ?c)"     => "(* -1 (% ?x ?c))" if crate::trs::is_not_zero("?c")),
+        rw!("mod-minus-in"  ; "(* -1 (% ?x ?c))"     => "(% (* ?x -1) ?c)" if crate::trs::is_not_zero("?c")),
         rw!("mod-two"       ; "(% (- ?x ?y) 2)"      => "(% (+ ?x ?y) 2)"),
         //FOLD
         rw!("mod-consts"    ; "( % ( + ( * ?x ?c0 ) ?y ) ?c1 )" => "( % ?y ?c1 )" if crate::trs::compare_c0_c1("?c0", "?c1", "%0")),
diff --git a/src/rules/mul.rs b/src/rules/mul.rs
index a1e0218..80d9c90 100644
--- a/src/rules/mul.rs
+++ b/src/rules/mul.rs
@@ -9,8 +9,8 @@ pub fn mul() -> Vec<Rewrite> {
         rw!("mul-assoc"     ; "(* ?a (* ?b ?c))"            => "(* (* ?a ?b) ?c)"),
         rw!("mul-zero"      ; "(* ?a 0)"                    => "0"),
         rw!("mul-one"       ; "(* ?a 1)"                    => "?a"),
-        rw!("mul-cancel-div"; "(* (/ ?a ?b) ?b)"            => "(- ?a (% ?a ?b))"),
+        rw!("mul-cancel-div"; "(* (/ ?a ?b) ?b)"            => "(- ?a (% ?a ?b))" if crate::trs::is_not_zero("?b")),
         rw!("mul-max-min"   ; "(* (max ?a ?b) (min ?a ?b))" => "(* ?a ?b)"),
-        rw!("div-cancel-mul"; "(/ (* ?y ?x) ?x)"            => "?y"),
+        rw!("div-cancel-mul"; "(/ (* ?y ?x) ?x)"            => "?y" if crate::trs::is_not_zero("?x")),
     ]
 }
diff --git a/src/trs/mod.rs b/src/trs/mod.rs
index bf2e477..dbc8111 100644
--- a/src/trs/mod.rs
+++ b/src/trs/mod.rs
@@ -223,18 +223,19 @@ pub fn compare_c0_c1(
                     "<a" => c < &c1.abs(),
                     "<=" => c <= c1,
                     "<=+1" => c <= &(c1 + 1),
-                    "<=a" => c <= &c1.abs(),
-                    "<=-a" => c <= &(-c1.abs()),
-                    "<=-a+1" => c <= &(1 - c1.abs()),
+                    "<=a" => c <= &c1.abs() && c1 != &0,
+                    "<=-a" => c <= &(-c1.abs()) && c1 != &0,
+                    "<=-a+1" => c <= &(1 - c1.abs()) && c != &0,
                     ">" => c > c1,
-                    ">a" => c > &c1.abs(),
+                    // ">a" => c > &c1.abs(),
                     ">=" => c >= c1,
-                    ">=a" => c >= &(c1.abs()),
-                    ">=a-1" => c >= &(c1.abs() - 1),
+                    ">=a" => c >= &(c1.abs()) && c1 != &0,
+                    ">=a-1" => c >= &(c1.abs() - 1) && c1 != &0,
                     "!=" => c != c1,
                     "%0" => (*c1 != 0) && (c % c1 == 0),
                     "!%0" => (*c1 != 0) && (c % c1 != 0),
                     "%0<" => (*c1 > 0) && (c % c1 == 0),
+                    "%0<0" => (*c1 > 0) && (c % c1 == 0) && (c != &0),
                     "%0>" => (*c1 < 0) && (c % c1 == 0),
                     _ => false,
                 },