From bc76afef93e72f7d317c3420fb27c6393dadd1e6 Mon Sep 17 00:00:00 2001 From: Johann Rudloff Date: Thu, 18 Jul 2019 22:46:36 +0200 Subject: [PATCH] Use labelled assertions to get a REALLY useful unsat-core. --- test/nlcompare.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/test/nlcompare.ml b/test/nlcompare.ml index 07880e7..99b2252 100644 --- a/test/nlcompare.ml +++ b/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 () = -- 2.45.2