Function z3_sys::Z3_algebraic_add [−] [src]

pub unsafe extern "C" fn Z3_algebraic_add(
    c: Z3_context, 
    a: Z3_ast, 
    b: Z3_ast
) -> Z3_ast

Return the value a + b.

  • Precondition: Z3_algebraic_is_value(c, a)
  • Precondition: Z3_algebraic_is_value(c, b)
  • Postcondition: Z3_algebraic_is_value(c, result)

See also: