Z3Selection

fun Z3Selection()