module Lp = struct
let target = `&3 * zz_x + -- &1 * zz_y`;;
let target_bound = `-- &6938 / &10000`;;
let precision_constant = Int 100000;;
let ineqs = [
ASSUME (mk_le_ineq (mk_linear [(mk_real_int64 100000L); (mk_real_int64 100000L); (mk_real_int64 100000L); ] ["zz_x"; "zz_y"; "z"; ])(mk_real_int64 314160L)), (mk_real_int64 150000L);
ASSUME (mk_le_ineq (mk_linear [(mk_real_int64 100000L); (mk_real_int64 141421L); (negate (mk_real_int64 100000L)); ] ["zz_x"; "zz_y"; "z"; ])(mk_real_int64 173206L)), (mk_real_int64 150000L);
];;
let target_vars = [
ASSUME (mk_le_ineq (mk_linear [(mk_real_int64 100000L); ] ["zz_y"; ])(mk_real_int64 1000000L)), (mk_real_int64 50000L);
ASSUME (mk_le_ineq (mk_linear [(negate (mk_real_int64 100000L)); ] ["zz_y"; ])(negate (mk_real_int64 173205L))), (mk_real_int64 46213200000L);
];;


let var_ineqs = [
];;
let start = Sys.time();;
let result = prove_lp ineqs var_ineqs target_vars target_bound precision_constant;;
end;;
Sys.time() -. Lp.start;;
concl (Lp.result);;