Why does CVC4 SMT solver return unknown (incomplete)?-CodePudding

I am fiddling around with the CVC4 SMT solver online version (with lang = cvc4).

I am not using the standard SMT-LIB format, but the native language implemented by CVC4, because it's a lot simpler. However, I am not able to prove very straightforward and obvious statements. For example, the first CHECKSAT gives me sat (satisfiable), which is correct, but the second CHECKSAT gives me unknow.

OPTION "incremental";

ASSERT FORALL (k : INT): ((k > 5 AND k < 7) => (k = 6));

CHECKSAT; % this returns sat, okay!

arr: ARRAY INT OF REAL;
ASSERT arr[6] = 123;

ASSERT FORALL (k : INT): ((k > 5 AND k < 7) => (arr[k] = 123));

CHECKSAT; % this returns unknown, why?

Why is CVC4 not being able to prove such a simple predicate logic expression? As far as I understand, SMT checking is not decidable, and therefore, there is no program that can prove all correct statements. However, this seems to be a very simple case, so I think I am misunderstanding something.

CodePudding user response：

As you noted, quantifiers make the logic semi-decidable, and SMT solvers usually don't handle such problems all that well. In this particular case, however, --fmf-bound option seems to be effective. (That is run cvc4 --fmf-bound and you'll see it responds back sat). This parameter enables finite instantiation based on finite integer bounds, which happens to solve this case. Note that it may or may not work for other problems.

You can achieve the same by adding the following line to your script:

OPTION "fmf-bound";

For details see this paper: https://cvc4.cs.stanford.edu/papers/CADE24-2013/qi_for_fmf_reynolds_cade24.pdf