Bit-vector Support

[zhanghongce]

Hi I was wondering if eldarica has support for bit-vector extraction. Attached is a testcase that Z3 works but eldarica reports errors like

Error in conversion from Princess to Eldarica (ITerm): bv_extract(0, 0, P10) sublcass of class ap.parser.IFunApp

Thanks!

testcase-sp.zip

[pruemmer]

Thanks for the report, apparently this got broken in one of the last updates, and should be fixed in 6ef5943. Support for extract is still quite experimental though, we have not experimented much with those BV operations in the context of Horn solving yet.

philipp@hal5:~/tmp/eldarica/eldarica$ ./eld -abstract:off /tmp/wrapper.smt2  -ssol
Warning: ignoring get-model
Theories: ModuloArithmetic, GroebnerMultiplication
sat
(define-fun INV ((A Bool) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8)) (E (_ BitVec 8)) (F (_ BitVec 8)) (G Bool) (H Bool) (I (_ BitVec 2)) (J (_ BitVec 2)) (K (_ BitVec 1)) (L (_ BitVec 8)) (M (_ BitVec 2)) (N (_ BitVec 2)) (O (_ BitVec 1)) (P (_ BitVec 8)) (Q (_ BitVec 8)) (R (_ BitVec 2)) (S (_ BitVec 2)) (T (_ BitVec 2)) (U (_ BitVec 2)) (V Bool) (W (_ BitVec 8)) (X (_ BitVec 8)) (Y (_ BitVec 8)) (Z (_ BitVec 8)) (A1 Bool)) Bool (and (and (or (or (or (not (= J (_ bv1 2))) (not (= K (_ bv1 1)))) (not (= O (_ bv0 1)))) (not (= S (_ bv0 2)))) (or (or (not (= J (_ bv1 2))) (not (= K (_ bv1 1)))) (not (= S (_ bv0 2))))) (or (= S (_ bv2 2)) (or (or (or (or (or (and (= K (_ bv0 1)) (= O (_ bv0 1))) (and (= K (_ bv0 1)) (or (not (= N (_ bv1 2))) (not (= O (_ bv1 1)))))) (and (= O (_ bv0 1)) (= S (_ bv3 2)))) (and (= S (_ bv1 2)) (or (not (= N (_ bv1 2))) (not (= O (_ bv1 1)))))) (and (or (not (= J (_ bv1 2))) (not (= K (_ bv1 1)))) (or (not (= N (_ bv1 2))) (not (= O (_ bv1 1)))))) (and (or (not (= O (_ bv0 1))) (not (= S (_ bv3 2)))) (or (>= S 2) (and (= K (_ bv0 1)) (= O (_ bv0 1)))))))))

[zhanghongce]

Thank you for the prompt reply!