From fcc6e6c899bb5d3d7cd26563bcfbac08e22ae49e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 5 Sep 2022 03:17:13 -0700 Subject: [PATCH] doc bug --- src/sat/smt/bv_delay_internalize.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/bv_delay_internalize.cpp b/src/sat/smt/bv_delay_internalize.cpp index 0082efdd7..4100aea8e 100644 --- a/src/sat/smt/bv_delay_internalize.cpp +++ b/src/sat/smt/bv_delay_internalize.cpp @@ -75,7 +75,7 @@ namespace bv { /** \brief expose the multiplication circuit lazily. It adds clauses for multiplier output one by one to enforce - the semantics of multiplier semantics. + the semantics of multipliers. */ bool solver::check_lazy_mul(app* e, expr* arg_value, expr* mul_value) {