From 5a38bb3cfc84d36b7e9463976826f3eaa8a5138f Mon Sep 17 00:00:00 2001 From: Louis Rubet Date: Sat, 22 Apr 2017 11:21:55 +0200 Subject: [PATCH] #34: debug btor --- src/rpn-binary.h | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/rpn-binary.h b/src/rpn-binary.h index db9e57b..2207460 100644 --- a/src/rpn-binary.h +++ b/src/rpn-binary.h @@ -37,7 +37,8 @@ void btor() integer_t bin = getb(); - _stack->push_back(NULL, sizeof(number), cmd_number, true); - number* left = (number*)_stack->back(); + void* significand; + number* left = (number*)_stack->allocate_back(sizeof(number), cmd_number, MPFR_128BITS_STORING_LENGTH, &significand); + left->init(significand); left->set(bin); }