diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2020-09-15 21:31:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-09-15 23:31:10 -0500 |
| commit | e61c6ecf2e8c569d9f1b5f27ec1309371cc45cff (patch) | |
| tree | 339ec96158b78b7e998a6c4edd16a4127a7fe8aa /src/preprocessing/passes/bv_to_int.h | |
| parent | 85a3056bed70e226d9e17a1f5785d957628f9e26 (diff) | |
bv2int: support models in tests (#5068)
Previous changes in this preprocessing pass have already enabled model generation when using it.
However, the satisfiable tests still had --no-check-models.
The changes in this PR:
All --no-check-models from current tests for the preprocessing pass are removed.
Refactoring of the relevant part of the code.
Solves CVC4/cvc4-projects#128.
Remark: disabling white-spaces when reviewing this PR is recommended.
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); |