get-value errors with the smt2 backend when assertions have quantifiers

[remi-delmas-3000]

When sending a model with quantifiers in assertions to the SMT backend, when the analysis fails with counter examples, CBMC tries to retrieve the value of all assertions by sending get-value to the SMT solver. However in some casesz3 fails on these statements because quantifiers are not supported in get-value commands.

CBMC version:
Operating system:
Exact command line resulting in the issue:
What behaviour did you expect:
What happened instead:

[remi-delmas-3000]

@TGWDB I was finally able to reproduce:

#include <stdlib.h>
void foo(char *dst, const char *src, size_t n)
  __CPROVER_requires(__CPROVER_is_fresh(src, n))
  __CPROVER_requires(__CPROVER_is_fresh(dst, n))
  __CPROVER_assigns(__CPROVER_object_from(dst))
  __CPROVER_ensures(__CPROVER_forall{size_t j; j < n ==> dst[j] == src[j]})
{
  for(size_t i = 0; i < n; i++)
    __CPROVER_assigns(i, __CPROVER_object_from(dst))
      // commenting out the loop invariant to make the analysis fail and reveal the error
      // __CPROVER_loop_invariant(i <= n)
      // __CPROVER_loop_invariant(__CPROVER_forall{size_t j; j < i ==> dst[j] == src[j]})
    {
      dst[i] = src[i];
    }
}

int main()
{
  char *dst;
  char *src;
  size_t n;
  foo(dst, src, n);
  return 0;
}

goto-cc main.c
goto-instrument --dfcc main --enforce-contract foo --apply-loop-contracts --malloc-may-fail --malloc-fail-null a.out b.out
cbmc b.out --z3

The missing loop invariant makes the post condition fail, and z3 throws an error:

Runtime Convert SSA: 0.0292554s
Running SMT2 QF_AUFBV using Z3
SMT2 solver returned error message:
	"line 7081 column 16: invalid get-value term, term must be ground and must not contain quantifiers"
Runtime Solver: 0.43849s
Runtime decision procedure: 0.46795s

[NlightNFotis]

Hello,

A report on this one since I have been digging into this one for a bit:

• I have been unable to reproduce this across 4 systems (all MacOS based, 3 M1/M2 + 1 Intel based) - I get analysis results and no SMT solver issues.
• However, a concerning outcome is that across two of the machines (both M1 Macs) I get different analysis results:
  • On one of the machines, following the compilation instructions that @remi-delmas-3000 has posted, and against cbmc-5.88.1 and z3 version 4.12.2 - 64bit I get ** 2 of 54 failed (3 iterations), and
  • On the other machine, against the same configuration I get ** 1 of 54 failed (2 iterations).
  • The property with inconsistent result between the two machines is __CPROVER_contracts_write_set_check_assignment.assertion.1 line 767 ptr NULL or writable up to size.
  • I am not entirely sure what causes one of the machines to go for 3 iterations against 2 - I investigated for a bit but the results of my investigation are inconclusive.

[TGWDB]

I can reproduce on Ubuntu 20.04 on WSL. I'll explore/update further later.

[TGWDB]

@remi-delmas-3000 The linked draft PR resolves the problem (although it's unclear to me whether we should merge it, I don't know why lambdas should [not] be used for array comprehension). That said, it would be interesting to know the exact environment you're producing the error in, in particular the version(s) of z3. Fotis and I have different results on this and different versions of z3, also sometimes different results with the same version on different architectures/systems.

[TGWDB]

Note that further evidence suggests that this is an issue only with older versions of z3, the latest (4.12.2) does not have this problem. We propose closing this issue (and the draft PR) with the recommendation to update to a newer version of z3.

[remi-delmas-3000]

Hi @TGWDB I could confirm that using z3 v4.12.2 the problem goes away under both linux and macOS, event when using --trace to get the falsification witness.

Closing the issue.