let demorgan() =
  begin
    printf "\nDeMorgan\n";
    let ctx = mk_context [||] in
    let bool_sort = Z3.mk_bool_sort ctx in
    let symbol_x = Z3.mk_int_symbol ctx 0 in
    let symbol_y = Z3.mk_int_symbol ctx 1 in
    let x = Z3.mk_const ctx symbol_x bool_sort in
    let y = Z3.mk_const ctx symbol_y bool_sort in
  
    (* De Morgan - with a negation around: *)  
    (* !(!(x && y) <-> (!x || !y)) *)
    let not_x = Z3.mk_not ctx x in
    let not_y = Z3.mk_not ctx y in
    let x_and_y = Z3.mk_and ctx [|x;y|] in
    let ls = Z3.mk_not ctx x_and_y in
    let rs = Z3.mk_or ctx [|not_x;not_y|] in
    let conjecture = Z3.mk_iff ctx ls rs in
    let negated_conjecture = Z3.mk_not ctx conjecture in

    Z3.assert_cnstr ctx negated_conjecture;
    (match Z3.check ctx with
    | Z3.L_FALSE ->
      (* The negated conjecture was unsatisfiable, hence the conjecture is valid *)
      printf "DeMorgan is valid\n"
    | Z3.L_UNDEF ->
      (* Check returned undef *)
      printf "Undef\n"
    | Z3.L_TRUE ->
      (* The negated conjecture was satisfiable, hence the conjecture is not valid *)
      Printf.printf "DeMorgan is not valid\n");
    Z3.del_context ctx;
  end