Function z3_sys::Z3_mk_bvslt

pub unsafe extern "C" fn Z3_mk_bvslt(
    c: Z3_context, 
    t1: Z3_ast, 
    t2: Z3_ast
) -> Z3_ast

Two’s complement signed less than.

It abbreviates:

(or (and (= (extract[|m-1|:|m-1|] t1) bit1)
(= (extract[|m-1|:|m-1|] t2) bit0))
(and (= (extract[|m-1|:|m-1|] t1) (extract[|m-1|:|m-1|] t2))
(bvult t1 t2)))

The nodes t1 and t2 must have the same bit-vector sort.