scheck: mkvar() with target or input type

Most instructions have one associated type, the 'target type'.
Some, like compares, have another one too, the 'input type'.

So, when creating a bitvector from an instruction, we need to specify
the type in some way.

So, create an helper for both cases: mktvar() and mkivar().

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

1 files changed, 12 insertions, 0 deletions

diff --git a/scheck.c b/scheck.c
index 5e2b60ab..07b15a06 100644
--- a/scheck.c
+++ b/scheck.c
@@ -70,6 +70,18 @@ static BoolectorNode *mkvar(Btor *btor, BoolectorSort s, pseudo_t pseudo)
 	return pseudo->priv = n;
 }
 
+static BoolectorNode *mktvar(Btor *btor, struct instruction *insn, pseudo_t src)
+{
+	BoolectorSort s = get_sort(btor, insn->type, insn->pos);
+	return mkvar(btor, s, src);
+}
+
+static BoolectorNode *mkivar(Btor *btor, struct instruction *insn, pseudo_t src)
+{
+	BoolectorSort s = get_sort(btor, insn->itype, insn->pos);
+	return mkvar(btor, s, src);
+}
+
 static BoolectorNode *get_arg(Btor *btor, struct instruction *insn, int idx)
 {
 	pseudo_t arg = ptr_list_nth(insn->arguments, idx);