Ошибка в Z3 Datalog

Question

Для регистрации данных программы в Z3 на дне, результат запроса

(query (CallGraph invo heap):print-answer true) 

дается Z3 является:

sat 
(and (= (:var 0) #b011) (= (:var 1) #b1)) 

Однако, ответ должен быть

sat 
    (and (= (:var 0) #b1) (= (:var 1) #b011)) 

Я прав? это ошибка в Z3?

(set-option :fixedpoint.engine datalog) 
    (declare-rel VarPointsTo ((_ BitVec 4) (_ BitVec 3))) 
    (declare-rel Reachable ((_ BitVec 3))) 
    (declare-rel Alloc ((_ BitVec 4) (_ BitVec 3) (_ BitVec 3))) 
    (declare-rel Move ((_ BitVec 4) (_ BitVec 4))) 
    (declare-rel FldPointsTo ((_ BitVec 3) (_ BitVec 1) (_ BitVec 3))) 
    (declare-rel Store ((_ BitVec 4) (_ BitVec 4) (_ BitVec 4))) 
    (declare-rel StrMap ((_ BitVec 4) (_ BitVec 1))) 
    (declare-rel Load ((_ BitVec 4) (_ BitVec 4) (_ BitVec 4))) 
    (declare-rel VCall ((_ BitVec 4) (_ BitVec 1) (_ BitVec 3))) 
    (declare-rel CallGraph ((_ BitVec 1) (_ BitVec 3))) 
    (declare-rel InterProcAssign ((_ BitVec 4) (_ BitVec 4))) 
    (declare-rel FormalArg ((_ BitVec 3) (_ BitVec 1) (_ BitVec 4))) 
    (declare-rel ActualArg ((_ BitVec 1) (_ BitVec 1) (_ BitVec 4))) 
    (declare-rel FormalReturn ((_ BitVec 3) (_ BitVec 4))) 
    (declare-rel ActualReturn ((_ BitVec 1) (_ BitVec 4))) 
    (declare-var var (_ BitVec 4)) 
    (declare-var heap (_ BitVec 3)) 
    (declare-var methHeap (_ BitVec 3)) 
    (declare-var to (_ BitVec 4)) 
    (declare-var from (_ BitVec 4)) 
    (declare-var baseH (_ BitVec 3)) 
    (declare-var fld (_ BitVec 1)) 
    (declare-var base (_ BitVec 4)) 
    (declare-var toMethHeap (_ BitVec 3)) 
    (declare-var invo (_ BitVec 1)) 
    (declare-var inMethHeap (_ BitVec 3)) 
    (declare-var n (_ BitVec 1)) 

    (rule (=> (and (Reachable methHeap) (Alloc var heap methHeap))(VarPointsTo var heap))) 
    (rule (=> (and (Move to from) (VarPointsTo from heap))(VarPointsTo to heap))) 
    (rule (=> (and (Store base var from) (and (VarPointsTo from heap) (and (VarPointsTo base baseH) (StrMap var fld))))(FldPointsTo baseH fld heap))) 
    (rule (=> (and (Load to var base) (and (VarPointsTo base baseH) (and (FldPointsTo baseH fld heap) (StrMap var fld))))(VarPointsTo to heap))) 
    (rule (=> (and (VCall var invo inMethHeap) (and (Reachable inMethHeap) (VarPointsTo var toMethHeap)))(Reachable toMethHeap))) 
    (rule (=> (and (VCall var invo inMethHeap) (and (Reachable inMethHeap) (VarPointsTo var toMethHeap)))(CallGraph invo toMethHeap))) 
    (rule (=> (and (CallGraph invo methHeap) (and (FormalArg methHeap n to) (ActualArg invo n from)))(InterProcAssign to from))) 
    (rule (=> (and (CallGraph invo methHeap) (and (FormalReturn methHeap from) (ActualReturn invo to)))(InterProcAssign to from))) 
    (rule (=> (and (InterProcAssign to from) (VarPointsTo from heap))(VarPointsTo to heap))) 
    (rule (AlloC#b0001 #b001 #b010)) 
    (rule (AlloC#b0010 #b001 #b010)) 
    (rule (Reachable #b001)) 
    (rule (Reachable #b010)) 
    (rule (AlloC#b0011 #b011 #b001)) 
    (rule (AlloC#b0100 #b100 #b011)) 
    (rule (Move #b0101 #b0100)) 
    (rule (StrMap #b0110 #b1)) 
    (rule (Store #b0001 #b0110 #b0011)) 
    (rule (StrMap #b0111 #b1)) 
    (rule (Load #b1000 #b0111 #b0001)) 
    (rule (VCall #b1000 #b1 #b001)) 
    (rule (ActualReturn #b1 #b1001)) 

    (query (VarPointsTo var heap):print-answer true) 
    (query (CallGraph invo heap):print-answer true) 
    (query (Reachable heap):print-answer true) 

Answer 1

Это не появляется воспроизвести в версии Z3 зарегистрировалась в GitHub/z3prover/z3 мастер отрасли. Способ, которым двигатель связывает переменные индексы с именами переменных, был хрупким, и все еще может быть способ вызвать эту ошибку с новейшей версией Z3, хотя я не могу ее воспроизвести.

Бинарный API предоставляет более надежный API: один представляет запрос с одной или несколькими объявлениями предикатов (функция из C API называется Z3_fixedpoint_query_relations, а другие поддерживаемые языки программирования поддерживают аналогично названные функции).