mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
doc bug
This commit is contained in:
parent
8dc8de8ccd
commit
fcc6e6c899
|
@ -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) {
|
||||
|
|
Loading…
Reference in a new issue