Set-Logic in Z3 .NET API

Question

How do I use set-logic when using the .NET API function .parseSmtlib2String(String) when using Z3 version 3.1?

I always end up with a Z3Error-Exception.

Isn't it necessary in that case?

Answer 1

Unfortunately, the command (set-logic <symbol>) is not supported when using the API parseSmtlib2String.

We have this limitation because of technical reasons. In the textual interface, the command set-logic can only be used before the context is initialized. The context is initialized based on the selected logic. When the API parseSmtlib2String is used the context has already been initialized by the user. So, the command set-logic fails, and generates a parsing error.

I acknowledge this is not the ideal behavior. I will investigate alternatives.