From 6ab39319647009def8926da4c82ca340790fa4b9 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Wed, 9 Oct 2024 13:48:26 +0200 Subject: [PATCH] write_btor: only initialize array with const value when it is fully def * If all addresses of an array have the same initial value, they can be initialized in one go in btor with the constraint that the initial value must be fully const and thus can't have undef bits in --- backends/btor/btor.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 9cfd967e5..1c2d5132e 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -832,7 +832,10 @@ struct BtorWorker } } - if (constword) + // If not fully defined, undef bits should be able to take a + // different value for each address so we can't initialise from + // one value (and btor2parser doesn't like it) + if (constword && firstword.is_fully_def()) { if (verbose) btorf("; initval = %s\n", log_signal(firstword));