From aa890585cf75e9b0290544ba6d52457edc25d637 Mon Sep 17 00:00:00 2001 From: Christoph Kirsch Date: Wed, 29 May 2024 18:50:46 +0200 Subject: [PATCH] Option for printing non-sequential BTOR2 --- tools/rotor.c | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/tools/rotor.c b/tools/rotor.c index 6a74618e..b2ff3d8a 100644 --- a/tools/rotor.c +++ b/tools/rotor.c @@ -439,7 +439,7 @@ uint64_t first_input = 0; // indicates if input has been consumed for the first uint64_t any_input = 0; // indicates if any input has been consumed uint64_t printing_unrolled_model = 0; // indicates for how many steps model is unrolled -uint64_t printing_for_btormc = 1; // indicates if targeting non-sequential BMC or SMT +uint64_t printing_non_seq_btor2 = 0; // indicates if targeting non-sequential BTOR2 uint64_t* eval_bad_nid = (uint64_t*) 0; @@ -4847,7 +4847,7 @@ uint64_t eval_property(uint64_t core, uint64_t* line) { } else { if (printing_unrolled_model) { w = w + dprintf(output_fd, "; bad-start-%lu: %s\n\n", current_step, get_comment(line)); - if (printing_for_btormc) + if (printing_non_seq_btor2 == 0) print_line_advancing_nid(line); else { if (eval_bad_nid == UNUSED) @@ -12288,6 +12288,7 @@ uint64_t rotor_arguments() { char* unroll_model_option; char* load_code_option; char* print_comments_option; + char* printing_non_seq_btor2_option; evaluate_model_option = "-m"; debug_model_option = "-d"; @@ -12314,6 +12315,8 @@ uint64_t rotor_arguments() { print_comments_option = "-nocomments"; + printing_non_seq_btor2_option = "-smt"; + target_exit_code = atoi(peek_argument(0)); while (1) { @@ -12458,6 +12461,10 @@ uint64_t rotor_arguments() { } else if (string_compare(peek_argument(1), print_comments_option)) { printing_comments = 0; + get_argument(); + } else if (string_compare(peek_argument(1), printing_non_seq_btor2_option)) { + printing_non_seq_btor2 = 1; + get_argument(); } else if (string_compare(peek_argument(1), "-")) { get_argument();