only deal with eq comparison

mythril/laser/smt/bitvecfunc.py

@@ -64,12 +64,12 @@ def _comparison_helper(
 
     if not a.symbolic and not b.symbolic:
         return Bool(z3.BoolVal(operation(a.value, b.value)), annotations=union)
-
     if (
         not isinstance(b, BitVecFunc)
         or not a.func_name
         or not a.input_
         or not a.func_name == b.func_name
+        or str(operation) not in ("<built-in function eq>", "<built-in function ne>")
     ):
         return Bool(z3.BoolVal(default_value), annotations=union)
 

tests/laser/smt/bitvecfunc_test.py

@@ -1,4 +1,4 @@
-from mythril.laser.smt import Solver, symbol_factory, bitvec
+from mythril.laser.smt import Solver, symbol_factory, UGT, UGE, ULT, ULE
 import z3
 import pytest
 
@@ -42,10 +42,10 @@ def test_bitvecfunc_arithmetic(operation, expected):
         (operator.le, z3.sat),
         (operator.gt, z3.unsat),
         (operator.ge, z3.sat),
-        (bitvec.UGT, z3.unsat),
-        (bitvec.UGE, z3.sat),
-        (bitvec.ULT, z3.unsat),
-        (bitvec.ULE, z3.sat),
+        (UGT, z3.unsat),
+        (UGE, z3.sat),
+        (ULT, z3.unsat),
+        (ULE, z3.sat),
     ],
 )
 def test_bitvecfunc_bitvecfunc_comparison(operation, expected):