Z3 Prover увеличивает время и память в командной строке

Question

Я пытаюсь проверить, что 003-23-80.cnf выполнимо, используя Z3Prover. Я уже проверил, что это можно сделать с помощью Minisat, но это заняло около 2 часов и 500 МБ памяти.

В bash Я написал:

z3 -wcnf -st -T: 9000 -память: 500 003-23-80.cnf

Я считаю, что это должно увеличить время до 9000 секунд, а памяти до 500 мегабайт, но мой вывод не соответствует:

Terminal Выходные данные

Что я делаю не так?

Answer 1

Независимо от памяти / времени и пр. c .; если minisat говорит, что этот тест равен sat, а z3 говорит, что это unsat, то у одного из них есть ошибка! В зависимости от того, какой из них действительно ожидается, вы должны сообщить об этом как об ошибке неисправной стороне. (Если вы не уверены, просто сообщите об этом пользователям z3, указав, что они не согласны с минисатом. Используйте средство отслеживания проблем здесь: https://github.com/Z3Prover/z3/issues)