Something went wrong. Try again.
forked from gbury/dolmen
Something went wrong. Try again.
1234567891011File "tests/typing/errors/shadow/def_fun_param.smt2", line 2, character 23-30:2 | (define-fun f ((x Int) (x Int)) Bool (= x x)) ^^^^^^^Error Parameter `x` was already bound at line 2, character 15-22 as another parameter of the same function definitionHint: Shadowing between parameters in the same function definition in SMT-LIB2 has extremely un-inuitive semantics, and lead to partially specified functions. It definitely doesn't do what you expect and such definitions are therefore strongly discouraged. For more information, read https://github.com/SMT-LIB/SMT-LIB-2/issues/36