scheck: fix type of operands in casts

Casts were using the target type for their operands.

Fix this by using the new helper mkivar() for them.

Signed-off-by: Luc Van Oostenryck <luc.vanoostenryck@gmail.com>

1 files changed, 8 insertions, 10 deletions

diff --git a/scheck.c b/scheck.c
index 07b15a06..bb052d97 100644
--- a/scheck.c
+++ b/scheck.c
@@ -165,18 +165,16 @@ static void icmp(Btor *btor, struct instruction *insn)
 
 static void unop(Btor *btor, struct instruction *insn)
 {
-	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
-	BoolectorNode *t, *a;
+	pseudo_t src = insn->src;
+	BoolectorNode *t;
 
-	a = mkvar(btor, s, insn->src1);
-	if (!a)
-		return;
 	switch (insn->opcode) {
-	case OP_NEG:	t = boolector_neg(btor, a); break;
-	case OP_NOT:	t = boolector_not(btor, a); break;
-	case OP_SEXT:	t = sext(btor, insn, a); break;
-	case OP_ZEXT:	t = zext(btor, insn, a); break;
-	case OP_TRUNC:	t = slice(btor, insn, a); break;
+	case OP_SEXT:	t = sext(btor, insn, mkivar(btor, insn, src)); break;
+	case OP_ZEXT:	t = zext(btor, insn, mkivar(btor, insn, src)); break;
+	case OP_TRUNC:	t = slice(btor, insn, mkivar(btor, insn, src)); break;
+
+	case OP_NEG:	t = boolector_neg(btor, mktvar(btor, insn, src)); break;
+	case OP_NOT:	t = boolector_not(btor, mktvar(btor, insn, src)); break;
 	default:
 		fprintf(stderr, "unsupported insn: %s\n", show_instruction(insn));
 		return;