diff options
Diffstat (limited to 'src/preprocessing/passes/bv_to_int.h')
| -rw-r--r-- | src/preprocessing/passes/bv_to_int.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h index db2d08b7d..b84726878 100644 --- a/src/preprocessing/passes/bv_to_int.h +++ b/src/preprocessing/passes/bv_to_int.h @@ -289,11 +289,12 @@ class BVToInt : public PreprocessingPass * When a UF f is translated to a UF g, * we add a define-fun command to the smt-engine * to relate between f and g. + * We do the same when f and g are just variables. * This is useful, for example, when asking * for a model-value of a term that includes the * original UF f. - * @param bvUF the original function - * @param intUF the translated function + * @param bvUF the original function or variable + * @param intUF the translated function or variable */ void defineBVUFAsIntUF(Node bvUF, Node intUF); |