From: Luc Van Oostenryck <luc.vanoostenryck@xxxxxxxxx>
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 <luc.vanoostenryck@xxxxxxxxx>
---
scheck.c | 5 ++---
1 file changed, 2 insertions(+), 3 deletions(-)
diff --git a/scheck.c b/scheck.c
index d3ebddd6c2f5..5e2b60abb163 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:
--
2.32.0
