--finite-model-find --decision=internal
