Method: Z3::Expr.Le

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

.Le(a, b) ⇒ Object 



86
87
88
89
90
91
92
93
94
95
96
 
# File 'lib/z3/expr/expr.rb', line 86

def Le(a, b)
  a, b = coerce_to_same_sort(a, b)
  case a
  when ArithExpr
    BoolSort.new.new(LowLevel.mk_le(a, b))
  when BitvecExpr
    raise Z3::Exception, "Use #signed_le or #unsigned_le for Bitvec, not <="
  else
    raise Z3::Exception, "Can't compare #{a.sort} values"
  end
end