From 4da930b4909bc19530a59d7494f79c9f78bbac8b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 27 Jan 2022 10:50:48 -0800
Subject: [PATCH] #5794

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/bv_rewriter.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index dcd3ff234..f1b0afd45 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/src/ast/rewriter/bv_rewriter.cpp
@@ -2809,6 +2809,10 @@ br_status bv_rewriter::mk_bvsmul_no_overflow(unsigned num, expr * const * args,
 
     bool is_num1 = is_numeral(args[0], a0_val, bv_sz);
     bool is_num2 = is_numeral(args[1], a1_val, bv_sz);
+    if (bv_sz == 1) {
+        result = m().mk_bool_val(!(a0_val.is_one() && a1_val.is_one()));
+        return BR_DONE;
+    }
     if (is_num1 && (a0_val.is_zero() || a0_val.is_one())) {
         result = m().mk_true();
         return BR_DONE;