3 ms·
Not all theory fragments supported by Z3 are decidable: Z3 includes an incomplete decision procedure for non-linear real arithmetic [1]. [1] http://stackoverfl
by ulber 12y ago
Not all theory fragments supported by Z3 are decidable: Z3 includes an incomplete decision procedure for non-linear real arithmetic [1].
[1] http://stackoverflow.com/a/13898524 http://stackoverflow.com/a/13898524