Mysterious bug on lists and pairs

[shiatsumat]

The following SMT2 code is not accepted by HoIce, probably by a bug.

I tried the following code on HoIce. (Sorry for this noisy and messy bug report!)

(set-logic HORN)

(declare-datatypes ((Mut 1)) ((par (T) ((mut (cur T) (ret T))))))
(declare-datatypes ((List 1)) ((par (T) (nil (insert (head T) (tail (List T)))))))

(declare-fun inck (Int (Mut (List Int))) Bool)
(assert (forall ((k Int))
  (=> true
    (inck k (mut nil nil)))
))
(assert (forall ((k Int) (x Int) (xs (List Int)) (xs! (List Int)))
  (=> (inck k (mut xs xs!))
    (inck k (mut (insert x xs) (insert (+ x k) xs!))))
))

(declare-fun length ((List Int) Int) Bool)
(assert (forall ((dummy Int))
  (=> true (length nil 0))
))
(assert (forall ((n Int) (x Int) (xs (List Int)))
  (=> (length xs n) (length (insert x xs) (+ 1 n)))
))

(declare-fun sum ((List Int) Int) Bool)
(assert (forall ((dummy Int))
  (=> true (sum nil 0))
))
(assert (forall ((n Int) (x Int) (xs (List Int)))
  (=> (sum xs n) (sum (insert x xs) (+ x n)))
))

(assert (forall ((n Int) (l Int) (r Int) (k Int) (xs (List Int)) (xs! (List Int)))
  (=> (and (sum xs n) (length xs l) (inck k (mut xs xs!)) (sum xs! r))
    (= r (+ n (* k l))))
))

(check-sat)
(get-model)

Passing the code above to HoIce under z3 4.7.1, I will unexpectedly get the following error.

(error "
  solver error: "line 30 column 54: unknown function/constant mut"
")

Interestingly, when I just swap the two arguments of inck, I will get unsat.

unsat
(error "
  no model available
")

However, the expected answer is sat.

[AdrienChampion]

Thank you for your feedback!

This seems to be a bug indeed, unfortunately I have very little time these days to work on this.

In any case, it seems you are encoding basic functions using declare-fun / assert. I strongly encourage you to rewrite (some of) them using define-fun-rec. Definitely length, probably sum.

By doing this, hoice will be able to use these functions as atoms, meaning it will be able to create lemmas that mention the length or sum of your structures.

If you do not do this, then the only atoms hoice can use are those that mention the constructors of your datatype. This makes for very, very weak lemmas.

Be warned though that define-fun-rec-s raise the SMT-level complexity significantly. It should be fine for the example you provided though.

I hope my explanation is understandable, let me know if some points are not clear to you.

Thank you again for your interest in hoice!

[AdrienChampion]

I cannot reproduce the error on mut your report, either it came from a problem in z3 or from some bug in hoice that has been fixed since you posted this issue.

In any case, I don't see this problem with z3 4.8.4 and 4.8.7. With hoice's current version, the check-sat produces unknown which is legal. Unfortunately, it produces unknown for a bad reason: z3 returns unknown for one of the check-sat-s in the pre-processing, which does not prevent the rest of the analysis from running.
This comes from the way hoice handles errors, which needs to be revamped.

I tried switching inck's inputs as you suggested and still get unknown, for the same reason.

[shiatsumat]

By the combination of hoice 1.9.0 (the latest version) and z3 4.7.1, I reproduced the same error message.
This bug might be due to z3 4.7.1.
I still need to use z3 4.7.1 as a backend to solve CHCs with recursive data types (if I use it as a backend, hoice is generally good at solving CHCs with recursive data types, which helped my research a lot).