Method: Z3::Expr.Ge

Defined in:
lib/z3/expr/expr.rb

.Ge(a, b) ⇒ Object 



62
63
64
65
66
67
68
69
70
71
72
 
# File 'lib/z3/expr/expr.rb', line 62

def Ge(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_ge(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_ge or #unsigned_ge for Bitvec, not >="
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end