почему результат решения z3 horn неизвестен и почему это неизвестная причина

Question

Я использую z3 для проверки эквивалентности. Я пытаюсь использовать z3 horn solver, чтобы ускорить время решения z3, и я столкнулся со следующей проблемой:

Хочу проверить, совпадают ли две программы или нет. Логика двух программ - P1: a2 = a1 + 2, где a1 - вход, a2 - выход P2: b2 = b1 + 2, где b1 - вход, b2 - выход Тип a1, a2, b1, b2 - это битовый вектор 64. Формула такова, что forall (a1, b1), (a1 == b1) && (a2 == a1 + 2) && (b2 == b1 + 2) => (a2 == b2)

Если я использую решатель bv, результат будет sat. Однако, если я использую решатель рога, результат решения будетunknown, и причина в том

unknown
Uninterpreted 'a2' in <null>:
query!0(#1,#0) :- 
 (= a2 (bvadd (:var 1) #x0000000000000002)),
 (not (= a2 b2)),
 (= b2 (bvadd (:var 0) #x0000000000000002)),
 (= (:var 1) (:var 0)).

почему у этих двух решателей разные результаты? И почему неизвестен результат работы рожкового решателя?

Вот исходный код:

#include "z3++.h"
using namespace std;

int main() {
  z3::context ctx;
  z3::expr a1 = ctx.bv_const("a1", 64);
  z3::expr a2 = ctx.bv_const("a2", 64);
  z3::expr b1 = ctx.bv_const("b1", 64);
  z3::expr b2 = ctx.bv_const("b2", 64);

  z3::expr p1 = (a2 == a1 + 2);
  z3::expr p2 = (b2 == b1 + 2);
  z3::expr p_same_input = (a1 == b1);
  z3::expr p_post = (a2 == b2);
  z3::expr f = z3::implies(p_same_input && p1 && p2, p_post);

  z3::expr smt = z3::forall(a1, b1, f);
  z3::solver s(ctx, "HORN");  // set the solver as a horn solver
  s.add(smt);
  cout << s.check() << endl;
  cout << s.reason_unknown() << endl;
}