Search code examples
javaz3smt

Z3 Failing Even After Setting interactive-mode to True

I'm using the Z3 Java API to solve a smt file using the parseSMT2File() method. However, even if I set params.add("interactive-mode", true) and then solver.setParameters(params), Z3 throws the following error:

Exception in thread "main" com.microsoft.z3.Z3Exception: (error "line 276 column 23: model is not available")
(error "line 277 column 26: model is not available")
(error "line 279 column 15: command is only available in interactive mode, use command (set-option :interactive-mode true)")
(error "line 280 column 16: model is not available")
Solution

  • parseSMT2File() only parses the assertions from the file, and returns them as one expression. It doesn't run many commands, including check-sat, i.e. you have to call check() on the solver that you added the assertion to as well.