From 9c45467edd3fd871bf47c64eb933ec87a64ba2e5 Mon Sep 17 00:00:00 2001
From: Yoni Zohar <yoni206@gmail.com>
Date: Thu, 1 Aug 2024 22:30:45 -0700
Subject: [PATCH] handling overflows

---
 src/theory/bv/int_blaster.cpp | 52 +++++++++++++++++++++++++++++++++++
 1 file changed, 52 insertions(+)

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index f7137f05ae4..06eb49074e4 100644
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -541,6 +541,58 @@ Node IntBlaster::translateWithChildren(
           d_zero);
       break;
     }
+    case Kind::BITVECTOR_UADDO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node sum = d_nm->mkNode(Kind::ADD, translated_children[0], translated_children[1]);
+      returnNode = d_nm->mkNode(Kind::GEQ, sum, pow2(bvsize));
+      break;
+    }
+    case Kind::BITVECTOR_SADDO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node signed0 = uts(translated_children[0], bvsize);
+      Node signed1 = uts(translated_children[1], bvsize);
+      Node sum = d_nm->mkNode(Kind::ADD, signed0, signed1);
+      Node disj1 = d_nm->mkNode(Kind::GEQ, sum, pow2(bvsize - 1));
+      Node disj2 = d_nm->mkNode(Kind::LT, sum, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
+      returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
+      break;
+    }
+    case Kind::BITVECTOR_UMULO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node mul = d_nm->mkNode(Kind::MULT, translated_children[0], translated_children[1]);
+      returnNode = d_nm->mkNode(Kind::GEQ, mul, pow2(bvsize));
+      break;
+    }
+    case Kind::BITVECTOR_SMULO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node signed0 = uts(translated_children[0], bvsize);
+      Node signed1 = uts(translated_children[1], bvsize);
+      Node mul = d_nm->mkNode(Kind::MULT, signed0, signed1);
+      Node disj1 = d_nm->mkNode(Kind::GEQ, mul, pow2(bvsize - 1));
+      Node disj2 = d_nm->mkNode(Kind::LT, mul, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
+      returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
+      break;
+    }
+    case Kind::BITVECTOR_USUBO:
+    {
+      returnNode = d_nm->mkNode(Kind::LT, translated_children[0], translated_children[1]);
+      break;
+    }
+    case Kind::BITVECTOR_SSUBO:
+    {
+      uint32_t bvsize = original[0].getType().getBitVectorSize();
+      Node signed0 = uts(translated_children[0], bvsize);
+      Node signed1 = uts(translated_children[1], bvsize);
+      Node sub = d_nm->mkNode(Kind::SUB, signed0, signed1);
+      Node disj1 = d_nm->mkNode(Kind::GEQ, sub, pow2(bvsize - 1));
+      Node disj2 = d_nm->mkNode(Kind::LT, sub, d_nm->mkNode(Kind::NEG, pow2(bvsize - 1)));
+      returnNode = d_nm->mkNode(Kind::OR, disj1, disj2);
+      break;
+    }
     case Kind::ITE:
     {
       returnNode = d_nm->mkNode(oldKind, translated_children);