Z3 Proof mode

[EmilyOng]

let make_z3_expression1 () =
    print_endline "------------------------------------";
    let ctx = Z3.mk_context [("proof", "false")] in

    let v92 = Z3.Expr.mk_const_s ctx "v92" (Z3.Arithmetic.Integer.mk_sort ctx) in
    let v93 = Z3.Expr.mk_const_s ctx "v93" (list_int_sort ctx) in
    let v119 = Z3.Expr.mk_const_s ctx "v119" (Z3.Arithmetic.Integer.mk_sort ctx) in
    let v120 = Z3.Expr.mk_const_s ctx "v120" (Z3.Arithmetic.Integer.mk_sort ctx) in
    let v121 = Z3.Expr.mk_const_s ctx "v121" (list_int_sort ctx) in
    let v148 = Z3.Expr.mk_const_s ctx "v148" (Z3.Arithmetic.Integer.mk_sort ctx) in
    let v161 = Z3.Expr.mk_const_s ctx "v161" (Z3.Arithmetic.Integer.mk_sort ctx) in
    let v91 = Z3.Expr.mk_const_s ctx "v91" (Z3.Arithmetic.Integer.mk_sort ctx) in
    let xs = Z3.Expr.mk_const_s ctx "xs" (list_int_sort ctx) in
    let init = Z3.Expr.mk_const_s ctx "init" (Z3.Arithmetic.Integer.mk_sort ctx) in
    let res = Z3.Expr.mk_const_s ctx "res" (Z3.Arithmetic.Integer.mk_sort ctx) in

    let a1 =
      Z3.Boolean.mk_and ctx [
        Z3.Boolean.mk_eq ctx v93 v121;
        Z3.Boolean.mk_eq ctx v161 v119;
        Z3.Boolean.mk_eq ctx xs (Z3.Expr.mk_app ctx (get_fun_decl ctx "cons") [v120; v121]);
        Z3.Boolean.mk_eq ctx v161 v148;
        Z3.Boolean.mk_eq ctx xs (Z3.Expr.mk_app ctx (get_fun_decl ctx "cons") [v92; v93]);
        Z3.Boolean.mk_eq ctx v91 (Z3.Arithmetic.mk_add ctx [v92; init])
      ]
    in

    let r = Z3.Expr.mk_const_s ctx "r" (Z3.Arithmetic.Integer.mk_sort ctx) in

    let a2 = Z3.Quantifier.(
      expr_of_quantifier
        (mk_exists_const ctx [r]
            (Z3.Boolean.mk_and ctx [
              Z3.Boolean.mk_eq ctx r (Z3.Arithmetic.mk_add ctx [v120; v119]);
              Z3.Boolean.mk_eq ctx res (Z3.Arithmetic.mk_add ctx [r; init])
            ]) None [] [] None None)) in

    let a3 =
      Z3.Boolean.mk_implies ctx
        (Z3.Boolean.mk_and ctx [a1; Z3.Boolean.mk_eq ctx res (Z3.Arithmetic.mk_add ctx [v148; v91]); a1])
        a2
    in

    let expr = Z3.Boolean.mk_not ctx a3 in
    print_endline (Expr.to_string expr);
    let solver = Solver.mk_simple_solver ctx in
    Solver.add solver [expr];
    let status =
      Solver.check solver []
    in
    print_endline (Solver.string_of_status status);
    print_endline "------------------------------------" in ();

  make_z3_expression1 ();