diff options
| author | mudathirmahgoub <mudathirmahgoub@gmail.com> | 2020-05-19 16:24:59 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-05-19 16:24:59 -0500 |
| commit | c8f149fa83fa16f821f37687fedfa778808809bd (patch) | |
| tree | 8808ec522b58c0d8273280923b984a72e0b7bb29 /src/theory/quantifiers/fmf/bounded_integers.h | |
| parent | 6bb98062a5578d126db6a3e8cdca083881893b32 (diff) | |
Renamed operator CHOICE to WITNESS (#4207)
Renamed operator CHOICE to WITNESS, and removed it from the front end
Diffstat (limited to 'src/theory/quantifiers/fmf/bounded_integers.h')
| -rw-r--r-- | src/theory/quantifiers/fmf/bounded_integers.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 1333af61c..2180a7270 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -72,7 +72,7 @@ private: * * For each set S and integer n, d_setm_choice[S][n] is the canonical * representation for the (n+1)^th member of set S. It is of the form: - * choice x. (|S| <= n OR ( x in S AND + * witness x. (|S| <= n OR ( x in S AND * distinct( x, d_setm_choice[S][0], ..., d_setm_choice[S][n-1] ) ) ) */ std::map<Node, std::vector<Node> > d_setm_choice; |