diff --git a/Changelog.md b/Changelog.md
index eefabf7d6..2a849b455 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -10,6 +10,7 @@ Compiler Features:
 Bugfixes:
  * SMTChecker: Fix internal error when using the custom NatSpec annotation to abstract free functions.
  * TypeChecker: Also allow external library functions in ``using for``.
+ * SMTChecker: Fix internal error caused by unhandled ``z3`` expressions that come from the solver when bitwise operators are used.
 
 
 ### 0.8.18 (2023-02-01)
diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp
index 4abeffa16..21b31d19f 100644
--- a/libsmtutil/Z3Interface.cpp
+++ b/libsmtutil/Z3Interface.cpp
@@ -344,6 +344,12 @@ Expression Z3Interface::fromZ3Expr(z3::expr const& _expr)
 		return arguments[0] % arguments[1];
 	else if (kind == Z3_OP_XOR)
 		return arguments[0] ^ arguments[1];
+	else if (kind == Z3_OP_BOR)
+		return arguments[0] | arguments[1];
+	else if (kind == Z3_OP_BAND)
+		return arguments[0] & arguments[1];
+	else if (kind == Z3_OP_BXOR)
+		return arguments[0] ^ arguments[1];
 	else if (kind == Z3_OP_BNOT)
 		return !arguments[0];
 	else if (kind == Z3_OP_BSHL)
diff --git a/test/libsolidity/smtCheckerTests/operators/bitwise_operators_do_not_throw_exceptions.sol b/test/libsolidity/smtCheckerTests/operators/bitwise_operators_do_not_throw_exceptions.sol
new file mode 100644
index 000000000..267705a0e
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/operators/bitwise_operators_do_not_throw_exceptions.sol
@@ -0,0 +1,12 @@
+contract C {
+    // tests that bitwise operators are parsed from z3 answer
+    function test(uint x, uint y) public pure {
+        x | y;
+        x & y;
+        x ^ y;
+        assert(true);
+    }
+}
+// ====
+// SMTEngine: all
+// ----