From 8caf71acab0e5ecc1db6949fb23be8a239729318 Mon Sep 17 00:00:00 2001
From: Aman Goel <goelaman@amazon.com>
Date: Fri, 30 Aug 2024 01:24:51 +0000
Subject: [PATCH] Minor

---
 src/vwn/btor2_frontend.cpp | 38 +++++++++++++++++++-------------------
 1 file changed, 19 insertions(+), 19 deletions(-)

diff --git a/src/vwn/btor2_frontend.cpp b/src/vwn/btor2_frontend.cpp
index f0feedb..a4f1885 100644
--- a/src/vwn/btor2_frontend.cpp
+++ b/src/vwn/btor2_frontend.cpp
@@ -496,12 +496,12 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
 			btor2_loge("negative boolean number isn't allowed: found in BTOR2_TAG_const " << snum);
 		}
 		node = NumInst::create(snum, sz, 2, sort);
-		{
-			string numstr = NumInst::as(node)->get_mpz()->get_str(2);
-			if (numstr != snum) {
-				btor2_loge("number error: gave " << snum << ", got " << numstr);
-			}
-		}
+		// {
+		// 	string numstr = NumInst::as(node)->get_mpz()->get_str(2);
+		// 	if (numstr != snum) {
+		// 		btor2_loge("number error: gave " << snum << ", got " << numstr);
+		// 	}
+		// }
 		constants.insert(node);
 		done = true;
 	} break;
@@ -525,25 +525,25 @@ void Btor2Frontend::get_node(NODE_INFO& info, InstL& args) {
 		} else {
 			node = NumInst::create(snum, sz, 10, sort);
 		}
-		if (sz != 1)
-		{
-			string numstr = NumInst::as(node)->get_mpz()->get_str(10);
-			if (numstr != snum) {
-				btor2_loge("number error: gave " << snum << ", got " << numstr);
-			}
-		}
+		// if (sz != 1)
+		// {
+		// 	string numstr = NumInst::as(node)->get_mpz()->get_str(10);
+		// 	if (numstr != snum) {
+		// 		btor2_loge("number error: gave " << snum << ", got " << numstr);
+		// 	}
+		// }
 		constants.insert(node);
 		done = true;
 	} break;
 	case BTOR2_TAG_consth: {
 		string snum(t.constant);
 		node = NumInst::create(snum, sz, 16, sort);
-		{
-			string numstr = NumInst::as(node)->get_mpz()->get_str(16);
-			if (numstr != snum) {
-				btor2_loge("number error: gave " << snum << ", got " << numstr);
-			}
-		}
+		// {
+		// 	string numstr = NumInst::as(node)->get_mpz()->get_str(16);
+		// 	if (numstr != snum) {
+		// 		btor2_loge("number error: gave " << snum << ", got " << numstr);
+		// 	}
+		// }
 		constants.insert(node);
 		done = true;
 	} break;