From 07e2ca100d5db4639a8b34c0c4ca5014c14a3da6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 23 Apr 2021 10:05:08 -0700 Subject: [PATCH] fix #5213 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index d01ed8b75..645088e3e 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -718,7 +718,7 @@ void bv_decl_plugin::get_op_names(svector & op_names, symbol const op_names.push_back(builtin_name("rotate_right",OP_ROTATE_RIGHT)); op_names.push_back(builtin_name("bit2bool", OP_BIT2BOOL)); - if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD") { + if (logic == symbol::null || logic == symbol("ALL") || logic == "QF_FD" || logic == "HORN") { op_names.push_back(builtin_name("bvumul_noovfl",OP_BUMUL_NO_OVFL)); op_names.push_back(builtin_name("bvsmul_noovfl",OP_BSMUL_NO_OVFL)); op_names.push_back(builtin_name("bvsmul_noudfl",OP_BSMUL_NO_UDFL));