diff options
Diffstat (limited to 'test/regress/regress1/fmf/agree467.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/agree467.smt2 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress1/fmf/agree467.smt2 b/test/regress/regress1/fmf/agree467.smt2 index 522609b11..f2b012c86 100644 --- a/test/regress/regress1/fmf/agree467.smt2 +++ b/test/regress/regress1/fmf/agree467.smt2 @@ -258,10 +258,10 @@ (assert (forall ((mk_array_7_index node$type)) (= (select mk_array_7 mk_array_7_index) null_state))) (define-fun null_state_set () state_set$type mk_array_7) -(declare-fun choose (Values$t$type) value$type) +(declare-fun set.choose (Values$t$type) value$type) ;choosen_value : (assert (forall ((vals Values$t$type)) (or (= vals Values$empty) (= (Values$mem - (choose + (set.choose vals) vals) Truth)))) |