1 files changed, 3 insertions(+), 3 deletions(-)

M test/nlcompare.ml

@@ 12,12 12,12 @@ module StrSet = Set.Make(String)
 let curry f = fun (a,b) -> f a b
 
 let write_smtlib_comparison write nl_a nl_b =
-  write "(set-option :produce-proofs true)\n(declare-sort Net)\n";
+  write "(set-option :produce-unsat-cores true)\n(set-option :produce-proofs true)\n(declare-sort Net)\n";
   let write_asserts nl nlname1 nlname2 =
     let prefix1 = nlname1 ^ "__" in
     let prefix2 = nlname2 ^ "__" in
     let write_generic_device name nets = List.iteri (fun i _ ->
-      write (Printf.sprintf "(assert (= %scomp_%s_pin_%d %scomp_%s_pin_%d))\n" prefix1 name i prefix2 name i)
+      write (Printf.sprintf "(assert (! (= %scomp_%s_pin_%d %scomp_%s_pin_%d) :named comp_%s_pin_%d_match))\n" prefix1 name i prefix2 name i name i)
     ) nets in
     let write_device name = let open Device in function
       | Resistor c -> write_generic_device name [c.net_neg;c.net_pos]


@@ 61,7 61,7 @@ let write_smtlib_comparison write nl_a nl_b =
   write_netlist nl_a "a";
   write_netlist nl_b "b";
   write_asserts nl_a "a" "b";
-  write "(check-sat)\n(get-model)\n(get-proof)\n"
+  write "(check-sat)\n(get-unsat-core)\n;(get-model)\n;(get-proof)\n"
 
 
 let test () =