diff --git a/Changelog.md b/Changelog.md
index 7619fbd40..bff045843 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
 
 Bugfixes:
  * 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
+// ----