From 918e9a4cface92c0a2ccec9479ef1ff77d75f18d Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Jul 2021 22:04:58 +0200 Subject: scheck: constants are untyped in sparse, constants (PSEUDO_VALs) are not typed, so the same pseudo can be used to represent 1-bit 0, 8-bit 0, 16-bit 0, ... That's incompatible with the bit vectors used here, so we can't associate a PSEUDO_VAL with its own bitvector like it's done for PSEUDO_REGs. A fresh one is needed for each occurrence (we could use a small table but won't bother). Signed-off-by: Luc Van Oostenryck --- scheck.c | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/scheck.c b/scheck.c index d3ebddd6..5e2b60ab 100644 --- a/scheck.c +++ b/scheck.c @@ -53,15 +53,14 @@ static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo) static char buff[33]; BoolectorNode *n; - if (pseudo->priv) - return pseudo->priv; - switch (pseudo->type) { case PSEUDO_VAL: sprintf(buff, "%llx", pseudo->value); return boolector_consth(btor, s, buff); case PSEUDO_ARG: case PSEUDO_REG: + if (pseudo->priv) + return pseudo->priv; n = boolector_var(btor, s, show_pseudo(pseudo)); break; default: -- cgit 1.2.3-korg