Error for unsat proof

[izumitanaka]

HoIce is aborted with:

asked for unsat proof while learning data is not unsat
while checking unsat result in teacher

for the input below.
Does this work as expected?

(set-logic HORN)


(declare-fun |main@empty.loop| ( Int (Array Int Int) Int ) Bool)
(declare-fun |main@verifier.error.split| ( ) Bool)
(declare-fun |main@_11| ( Int Int (Array Int Int) Int ) Bool)
(declare-fun |main@init.exit| ( (Array Int Int) ) Bool)

(assert
  (forall ( (A (Array Int Int)) ) 
    (=>
      (and
        true
      )
      (main@init.exit A)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) (B Bool) (C (Array Int Int)) (D Int) (E (Array Int Int)) (F Int) (G (Array Int Int)) (H Int) (I (Array Int Int)) (J Int) (K (Array Int Int)) (L Int) (M (Array Int Int)) (N Int) (O (Array Int Int)) (P Int) (Q (Array Int Int)) (R Int) (S (Array Int Int)) (T Int) (U (Array Int Int)) (V Int) (W Bool) (X Bool) (Y Int) (Z (Array Int Int)) (A1 Int) ) 
    (=>
      (and
        (main@init.exit A)
        (and (= P (+ 24 Y))
     (= J (+ 12 Y))
     (= F (+ 4 Y))
     (= L (+ 16 Y))
     (= T (+ 32 Y))
     (= N (+ 20 Y))
     (= H (+ 8 Y))
     (= V (+ 36 Y))
     (= D Y)
     (= R (+ 28 Y))
     (= Z (store U V 0))
     (= I (store G H 0))
     (= E (store C D 0))
     (= S (store Q R 0))
     (= O (store M N 0))
     (= U (store S T 0))
     (= C A)
     (= Q (store O P 0))
     (= M (store K L 0))
     (= K (store I J 0))
     (= G (store E F 0))
     (not (<= Y 0))
     (or (not (<= P 0)) (<= Y 0))
     (or (<= Y 0) (not (<= J 0)))
     (or (not (<= F 0)) (<= Y 0))
     (or (<= Y 0) (not (<= L 0)))
     (or (<= Y 0) (not (<= T 0)))
     (or (<= Y 0) (not (<= N 0)))
     (or (<= Y 0) (not (<= H 0)))
     (or (not (<= V 0)) (<= Y 0))
     (or (<= Y 0) (not (<= D 0)))
     (or (not (<= R 0)) (<= Y 0))
     (or (not X) (and W X))
     (= X true)
     (= B true)
     (= B (= A1 0)))
      )
      (main@empty.loop Y Z A1)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) (D Bool) (E Int) (F (Array Int Int)) (G Int) ) 
    (=>
      (and
        (main@empty.loop E F G)
        (and (or (not D) (and C D))
     (or (not C) (and A C))
     (= D true)
     (or (not C) (not A) B))
      )
      (main@empty.loop E F G)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) (F Int) (G (Array Int Int)) (H Int) ) 
    (=>
      (and
        (main@empty.loop F G H)
        (and (or (not D) (= C 0) (not B))
     (or (not D) (not B) (not A))
     (or (not D) (and B D))
     (= D true)
     (or (not D) (not B) (= E C)))
      )
      (main@_11 E F G H)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C Int) (D Int) (E Bool) (F Int) (G Bool) (H Int) (I Bool) (J Int) (K Int) (L (Array Int Int)) (M Int) ) 
    (=>
      (and
        (main@_11 D K L M)
        (and (= E (= C M))
     (= B (+ K (* 4 D)))
     (= F (+ 1 D))
     (= C (select L B))
     (not (<= K 0))
     (or (not I) (not G) (= J H))
     (or (= H F) (not I) (not G))
     (or (not I) E (not G))
     (or (not (<= B 0)) (<= K 0))
     (or (not I) (and G I))
     (= A true)
     (= I true)
     (not (= (<= 10 D) A)))
      )
      (main@_11 J K L M)
    )
  )
)
(assert
  (forall ( (A Bool) (B Int) (C (Array Int Int)) (D Int) (E Int) (F Int) (G Int) (H Int) (I Bool) (J Bool) (K Bool) (L Bool) ) 
    (=>
      (and
        (main@_11 H B C F)
        (and (= J (= E F))
     (= D (+ B (* 4 H)))
     (= E (select C D))
     (= G (+ 1 H))
     (not (<= B 0))
     (or (not K) (not J) (not I))
     (or (not (<= D 0)) (<= B 0))
     (or (not L) (and K L))
     (or (not K) (and K I))
     (= L true)
     (= A true)
     (not (= (<= 10 H) A)))
      )
      main@verifier.error.split
    )
  )
)
(assert
  (forall ( (CHC_COMP_UNUSED Bool) ) 
    (=>
      (and
        main@verifier.error.split
        true
      )
      false
    )
  )
)

(check-sat)
(exit)

[AdrienChampion]

The problem seems to be that hoice cannot answer the check-sat and crashes as it tries to produce an unknown result.

Fixed by #66

[AdrienChampion]

I haven't checked that unknown is actually the expected result, which would mean that hoice's qualifiers are not good enough to build proper candidates on this instance. Feel free to re-open the issue if you think hoice should be able to synthesize better candidates