bveq

Author: katrinafyi

src/main/scala/translating/GTIRBToIR.scala

@@ -353,7 +353,7 @@ class GTIRBToIR(
     }
 
     block.address.foreach { case addr =>
-      val pcCorrectExpr = BinaryExpr(BVEQ, Register("_PC", 64), BitVecLiteral(addr, 64))
+      val pcCorrectExpr = BinaryExpr(EQ, Register("_PC", 64), BitVecLiteral(addr, 64))
       val assertPC = Assert(pcCorrectExpr, None, Some("pc-tracking"))
       block.statements.append(assertPC)
     }

src/main/scala/util/RunUtils.scala

@@ -1169,8 +1169,8 @@ object RunUtils {
         val pcVar = BVariable("_PC", BitVecBType(64), Scope.Global)
         val r30Var = BVariable("R30", BitVecBType(64), Scope.Global)
         val addrVar = BitVecBLiteral(addr, 64)
-        val pcRequires = BinaryBExpr(BVEQ, pcVar, addrVar)
-        val pcEnsures = BinaryBExpr(BVEQ, pcVar, Old(r30Var))
+        val pcRequires = BinaryBExpr(EQ, pcVar, addrVar)
+        val pcEnsures = BinaryBExpr(EQ, pcVar, Old(r30Var))
 
         val name = proc.procName
         (name -> SubroutineSpec(name, requires = List(pcRequires), ensures = List(pcEnsures)))