Horn engine timeout with simple query involving bitvectors

[grievejia]

Here's my query encoded in the muz format:

(set-logic HORN)
(declare-rel $END_QUERY ())
(declare-rel INV_REL
 ((_ BitVec 32) Int (_ BitVec 32)
  (_ BitVec 32) Int (_ BitVec 32)))
(declare-var i Int)
(declare-var i.2 Int)
(declare-var n (_ BitVec 32))
(declare-var n.0 (_ BitVec 32))
(declare-var x (_ BitVec 32))
(declare-var x.3 (_ BitVec 32))

(rule
 (=>
  (and(= n.0 n) (INV_REL n.0 i.2 x.3 n i x)
   (>= i.2 7) (>= i 7) (not (= x.3 x)))
  $END_QUERY))

(rule
 (=>
  (and (< i.2 7) (>= i 7) (INV_REL n.0 i.2 x.3 n i x))
  $END_QUERY))

(rule
 (=>
  (and (>= i.2 7) (< i 7) (INV_REL n.0 i.2 x.3 n i x))
  $END_QUERY))

(rule
 (=> (= n.0 n) (INV_REL n.0 0 (_ bv0 32) n 0 (_ bv0 32))))

(rule
 (let ((x.3$2 (bvor (bvshl x.3 (_ bv4 32)) (bvudiv (_ bv0 32) n.0))))
  (let ((i.2$2 (+ i.2 1)))
   (let ((x$2 (bvor (bvshl x (_ bv4 32)) (bvudiv (_ bv0 32) n))))
    (let ((i$2 (+ i 1)))
     (=>
      (and (< i.2 7) (< i 7) (INV_REL n.0 i.2 x.3 n i x))
      (INV_REL n.0 i.2$2 x.3$2 n i$2 x$2)))))))

(query $END_QUERY)

The expected answer is unsat. I tried pdr, gpdr, spacer and duality, and all of them would hang on this simple example.

This problem originally comes from the application domain of equivalence checking: I want to verify the equivalence of the following two procedures:

uint32_t f0(uint32_t n) {
  uint32_t x = 0, y = 0;
  for (int i = 0; i < 7; i++) {
    x = ((x << 4) | (y / n));
  }
  return x;
}

uint32_t f1(uint32_t n_0) {
  uint32_t x_3 = 0, y_4 = 0;
  for (int i_2 = 0; i_2 < 7; i_2++) {
    x_3 = ((x_3 << 4) | (y_4 / n));
  }
  return x_3;
}

To me this seems to be an easy problem: the unknown predicate INV_REL could just be set to i == i_2 && x == x_3 to solve the query. I'm not a horn solver expert so I'm not sure what makes the problem so hard for the horn engine. Is there any simple thing I can do (besides replacing y / n with 0 since that's not really a general solution) to make the problem solvable by Z3? Thanks in advance.

[NikolajBjorner]

Thanks for the example that integrates both arithmetical and bit-vector domains. The pdr engine understands bit-vectors but contains no features to synthesize useful word-level inductive invariants. The spacer engine does not yet work with bit-vectors, but should do so soon enough, but the first version may be as limited as the pdr engine when it comes to the ability to detect even simple word level invariants, but this example should be useful to drive this part.

[grievejia]

Thanks for the reply! I was not aware that bitvectors are not well supported in the horn engines. As a workaround I'll just model them as integers instead. On the other hand, I have more int-only examples where the horn engine hangs on somewhat simple problems. Here's one:

(set-logic HORN)
(declare-rel $END_QUERY ())
(declare-rel INV_REL$0
 ((Array Int Int) Int Int Int Int (Array Int Int) Int Int Int Int))
(declare-var a0 (Array Int Int))
(declare-var a1 (Array Int Int))
(declare-var i0 Int)
(declare-var i1 Int)
(declare-var r0 Int)
(declare-var r1 Int)
(declare-var t0 Int)
(declare-var t1 Int)
(declare-var x0 Int)
(declare-var x1 Int)
(rule
 (=>
  (and
   (and (and (< i0 1000) (<= x0 (select a0 i0)))
    (not (and (< i1 1000) (<= x1 (select a1 i1)))))
   (INV_REL$0 a0 x0 r0 i0 t0 a1 x1 r1 i1 t1))
  $END_QUERY))
(rule
 (=>
  (and
   (and (not (and (< i0 1000) (<= x0 (select a0 i0))))
    (and (< i1 1000) (<= x1 (select a1 i1))))
   (INV_REL$0 a0 x0 r0 i0 t0 a1 x1 r1 i1 t1))
  $END_QUERY))
(rule
 (=> (and (= a0 a1) (= x0 x1))
  (INV_REL$0 a0 x0 r0 0 0 a1 x1 r1 0 0)))
(rule
 (=>
  (and
   (< i0 1000) (<= x0 (select a0 i0))
   (< i1 1000) (<= x1 (select a1 i1))
   (INV_REL$0 a0 x0 r0 i0 t0 a1 x1 r1 i1 t1))
  (INV_REL$0 a0 x0 r0 (+ i0 1) t0 a1 x1 r1 (+ i1 1) t1)))
(rule
 (let ((t0$0 0))
   (let ((t1$2 0))
     (let ((r0$6 t0$0))
      (let ((r1$7 t1$2))
       (=>
        (and (= a0 a1) (= x0 x1)
         (INV_REL$0 a0 x0 r0 i0 t0$0 a1 x1 r1 i1 t1$2)
         (not (and (< i0 1000) (<= x0 (select a0 i0))))
         (not (and (< i1 1000) (<= x1 (select a1 i1))))
         (not (= r0$6 r1$7)))
        $END_QUERY))))))
(query $END_QUERY)

Again, the horn clauses comes from equivalence checking the following two functions:

int f0(int* a0, int x0) {
  int i0 = 0, t0 = 0;
  while (i0 < 1000 && x0 <= a0[i]) {
    i0++;
  }
  return t0;
}
int f1(int* a1, int x1) {
  int i1 = 0, t1 = 0;
  while (i1 < 1000 && x1 <= a1[i1]) {
    i1++;
  }
  return t1;
}

This problem looks rather trivial to me: the loop doesn't even touch the returned variable, and we are essentially asserting 0=0.