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 <luc.vanoostenryck@gmail.com>

1 files 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: