@@ -496,12 +496,12 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
496
496
btor2_loge (" negative boolean number isn't allowed: found in BTOR2_TAG_const " << snum);
497
497
}
498
498
node = NumInst::create (snum, sz, 2 , sort);
499
- {
500
- string numstr = NumInst::as (node)->get_mpz ()->get_str (2 );
501
- if (numstr != snum) {
502
- btor2_loge (" number error: gave " << snum << " , got " << numstr);
503
- }
504
- }
499
+ // {
500
+ // string numstr = NumInst::as(node)->get_mpz()->get_str(2);
501
+ // if (numstr != snum) {
502
+ // btor2_loge("number error: gave " << snum << ", got " << numstr);
503
+ // }
504
+ // }
505
505
constants.insert (node);
506
506
done = true ;
507
507
} break ;
@@ -525,25 +525,25 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
525
525
} else {
526
526
node = NumInst::create (snum, sz, 10 , sort);
527
527
}
528
- if (sz != 1 )
529
- {
530
- string numstr = NumInst::as (node)->get_mpz ()->get_str (10 );
531
- if (numstr != snum) {
532
- btor2_loge (" number error: gave " << snum << " , got " << numstr);
533
- }
534
- }
528
+ // if (sz != 1)
529
+ // {
530
+ // string numstr = NumInst::as(node)->get_mpz()->get_str(10);
531
+ // if (numstr != snum) {
532
+ // btor2_loge("number error: gave " << snum << ", got " << numstr);
533
+ // }
534
+ // }
535
535
constants.insert (node);
536
536
done = true ;
537
537
} break ;
538
538
case BTOR2_TAG_consth: {
539
539
string snum (t.constant );
540
540
node = NumInst::create (snum, sz, 16 , sort);
541
- {
542
- string numstr = NumInst::as (node)->get_mpz ()->get_str (16 );
543
- if (numstr != snum) {
544
- btor2_loge (" number error: gave " << snum << " , got " << numstr);
545
- }
546
- }
541
+ // {
542
+ // string numstr = NumInst::as(node)->get_mpz()->get_str(16);
543
+ // if (numstr != snum) {
544
+ // btor2_loge("number error: gave " << snum << ", got " << numstr);
545
+ // }
546
+ // }
547
547
constants.insert (node);
548
548
done = true ;
549
549
} break ;
0 commit comments