From d77d42aad4854d20a663e2a60657fe0f9e1d7231 Mon Sep 17 00:00:00 2001
From: Brendan Edmonds <bed88012@gmail.com>
Date: Tue, 12 Sep 2023 14:46:57 +1000
Subject: [PATCH] BASIL-1: Fixed review comments

---
 src/test/scala/BitVectorAnalysisTests.scala | 29 +++++----------------
 1 file changed, 7 insertions(+), 22 deletions(-)

diff --git a/src/test/scala/BitVectorAnalysisTests.scala b/src/test/scala/BitVectorAnalysisTests.scala
index 7d12ec123..668ea6c1a 100644
--- a/src/test/scala/BitVectorAnalysisTests.scala
+++ b/src/test/scala/BitVectorAnalysisTests.scala
@@ -11,11 +11,6 @@ class BitVectorAnalysisTests extends AnyFunSuite {
     assert(result == BigInt(2))
   }
 
-  test("Natural to BitVector - should return 0 when natural number does not fit within specified bit size") {
-    val result = nat2bv(8, BigInt(256))
-    assert(result == BitVecLiteral(BigInt(0), 8))
-  }
-
   test("Natural to BitVector - should return number when natural number does fit within specified bit size") {
     val result = nat2bv(8, BigInt(255))
     assert(result == BitVecLiteral(BigInt(255), 8))
@@ -26,11 +21,6 @@ class BitVectorAnalysisTests extends AnyFunSuite {
     assert(result == BitVecLiteral(18, 8))
   }
 
-  test("BitVector Add - should subtract two BitVectors when the second value is negative") {
-    val result = smt_bvadd(BitVecLiteral(255, 8), BitVecLiteral(-1, 8))
-    assert(result == BitVecLiteral(254, 8))
-  }
-
   test("BitVector Add - should throw exception when the result is negative") {
     intercept[IllegalArgumentException] {
       val result = smt_bvadd(BitVecLiteral(0, 8), BitVecLiteral(-1, 8))
@@ -42,6 +32,11 @@ class BitVectorAnalysisTests extends AnyFunSuite {
     assert(result == BitVecLiteral(0, 8))
   }
 
+  test("BitVector Add - should calculate the sum of two numbers that have a high bit count") {
+    val result = smt_bvadd(BitVecLiteral(BigInt("FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFE", 16), 128), BitVecLiteral(4, 128))
+    assert(result == BitVecLiteral(2, 128))
+  }
+
   // smt_bvmul
 
   test("BitVector Multiply - should return the product of two BitVectors") {
@@ -56,8 +51,8 @@ class BitVectorAnalysisTests extends AnyFunSuite {
   }
 
   test("BitVector Multiply - should return wrap BitVectors when sum is greater size number of bits") {
-    val result = smt_bvmul(BitVecLiteral(255, 8), BitVecLiteral(1, 8))
-    assert(result == BitVecLiteral(255, 8))
+    val result = smt_bvmul(BitVecLiteral(255, 8), BitVecLiteral(2, 8))
+    assert(result == BitVecLiteral(254, 8))
   }
   // smt_bvneg
 
@@ -71,11 +66,6 @@ class BitVectorAnalysisTests extends AnyFunSuite {
     assert(result == BitVecLiteral(0, 8))
   }
 
-  test("BitVector Negate - should return x when negating negative numbers") {
-    val result = smt_bvneg(BitVecLiteral(-3, 8))
-    assert(result == BitVecLiteral(3, 8))
-  }
-
   // smt_bvsub
 
   test("BitVector Subtract - should subtract two numbers ") {
@@ -161,11 +151,6 @@ class BitVectorAnalysisTests extends AnyFunSuite {
     assert(result == BitVecLiteral(BigInt("011", 2), 3))
   }
 
-  test("BitVector Extract - should extract bits from a given number when range is outside of bit given bit range") {
-    val result = smt_extract(7, 5, BitVecLiteral(BigInt("111011", 2), 6))
-    assert(result == BitVecLiteral(BigInt("001", 2), 3))
-  }
-
   // boogie_extract
 
   test("Boogie Extract - should extract bits from a given number") {