From d88cc139a029764cf62d95b2eaaff99e270a134a Mon Sep 17 00:00:00 2001 From: Makai Mann Date: Mon, 11 Nov 2019 16:40:51 -0800 Subject: [PATCH 1/2] Add an info string symbol for bad states in btor backend --- backends/btor/btor.cc | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 9e316a055..2babd454c 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1070,7 +1070,16 @@ struct BtorWorker bad_properties.push_back(nid_en_and_not_a); } else { int nid = next_nid++; - btorf("%d bad %d\n", nid, nid_en_and_not_a); + + string infostr = + cell->attributes.count("\\src") + ? cell->attributes.at("\\src") + .decode_string() + .c_str() + : log_id(cell); + + std::replace(infostr.begin(), infostr.end(), ' ', '_'); + btorf("%d bad %d %s\n", nid, nid_en_and_not_a, infostr.c_str()); } btorf_pop(log_id(cell)); From cd44826d5026316d9b44ae33c1fcf0d8faf550c4 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 14 Nov 2019 11:57:38 +0100 Subject: [PATCH 2/2] Use cell name for btor bad state props when it is a public name Signed-off-by: Clifford Wolf --- backends/btor/btor.cc | 14 +++++--------- 1 file changed, 5 insertions(+), 9 deletions(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 2babd454c..c1da4b127 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1070,15 +1070,11 @@ struct BtorWorker bad_properties.push_back(nid_en_and_not_a); } else { int nid = next_nid++; - - string infostr = - cell->attributes.count("\\src") - ? cell->attributes.at("\\src") - .decode_string() - .c_str() - : log_id(cell); - - std::replace(infostr.begin(), infostr.end(), ' ', '_'); + string infostr = log_id(cell); + if (infostr[0] == '$' && cell->attributes.count("\\src")) { + infostr = cell->attributes.at("\\src").decode_string().c_str(); + std::replace(infostr.begin(), infostr.end(), ' ', '_'); + } btorf("%d bad %d %s\n", nid, nid_en_and_not_a, infostr.c_str()); }