Pierre Villemot
Pierre Villemot
In my opinion we should deprecate this feature as we can reproduce this behaviour using the SMT-LIB language. We can deprecate the feature with the legacy frontend in 2.6.0 and...
I forgot to put `optimization` in the title ;)
I will check later for the incremental issue but clearly we should fix this at some point ;)
> That is unfortunate we have to do this even if we never call `(get-value)`; is there a chance we could call `cancel_until` at the moment `(get-value)` is called instead?...
> > Please either remove entirely `Sat_solver_util.Make` or separate the definition of `Satml_frontend.Make` in `Satml_frontend.Make_internal` followed by `Satml_frontend.Make(Th) = Sat_solver_util.Make(Make_internal(Th))`; the indentation changes make it virtually impossible to review changes...
> Why are all the tests calling `(get-value (true))`? This doesn't seem to be a very demanding test of the feature! Please add specific tests for `(get-value)` rather than tacking...
Finally, I added a new SMT option `:verify-models`. This option doesn't output a message in case of success.
> I am wondering if we should pass `--verify-models` in the tests (like we do `--enable-assertions`) rather than explicitly use `set-option` everywhere. This would mean that `--verity-models` does not imply...
I am not sure this file is correct: ```smt2 (declare-const x Int) (push 1) (assert (= x 42)) (check-sat) (get-value (x)) ; Should be 42 (pop 1) (assert (= x...
> Oh no! Is this because we use the boolean model? I think it's because of #1023