From 72d04aab864fa7b847a201ebfd229ce4842386e7 Mon Sep 17 00:00:00 2001 From: Luc Van Oostenryck Date: Fri, 9 Jul 2021 22:13:33 +0200 Subject: 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 --- scheck.c | 18 ++++++++---------- 1 file 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; -- cgit 1.2.3-korg