Следующий код SMT-LIB работает без проблем в Z3, MathSat и CVC4, но не работает в Alt-Ergo. Пожалуйста, дайте мне знать, что произойдет, большое спасибо: (set-logic QF_UF) (set-option :incremental true) (set-option :produce-models true)...

Mathsat поддерживает команду check-allsat , а Z3 ее не поддерживает. Пожалуйста, рассмотрите следующий пример: (declare-fun m () Bool) (declare-fun p () Bool) (declare-fun b () Bool) (declare-fun c () Bool) (declare-fun r () Bool) (declare-fun...