hopv/hoice

An ICE-based predicate synthesizer for Horn clauses.

hoice's Issues

hoice crush with "-v -v -v"

hoice crushes for the benchmark:
https://github.com/chc-comp/rust-horn/blob/master/trees-1-append-safe.smt2
when run with "-v -v -v".

$ hoice -v -v -v trees-1-append-safe.smt2 
; Running top pre-processing
; running simplify
...
; looking for counterexamples in implication clauses (3)...
;   extracted 2 cexs
;   generating data from initial cex...
;     trying to break
;     (%append.0 (~mut<%Tree> (as %Tree-1 %Tree) (as %Tree-1 %Tree)) (as %Tree-1 %Tree)) (%sum.0 (as %Tree-1 %Tree) 0) (%sum.0 (as %Tree-1 %Tree) (- 1)) => false
thread 'main' panicked at src/teacher/assistant.rs:264:33:
index out of bounds: the len is 0 but the index is 1
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

Hoice fails to generate unsat proof when the backend z3 version is 4.8.8

Input: smt2 file

(set-logic HORN)
(set-option :produce-proofs true)
(declare-fun X0 (Int) Bool)
(declare-fun X1 (Int) Bool)
(declare-fun X2 (Int) Bool)
(declare-fun X3 (Int) Bool)
(declare-fun X4 (Int) Bool)
(declare-fun X6 (Int) Bool)
(declare-fun X7 (Int) Bool)
(declare-fun X8 (Int) Bool)
(declare-fun X9 (Int) Bool)
(declare-fun X10 (Int) Bool)
(declare-fun X11 (Int) Bool)
(declare-fun X12 (Int) Bool)
(declare-fun X26 (Int Int) Bool)
(declare-fun X27 (Int Int) Bool)
(declare-fun X28 (Int Int) Bool)
(declare-fun X29 (Int Int) Bool)
(declare-fun X30 (Int Int) Bool)
(assert (forall ((n4 Int)) (=> true (X0  n4))))
(assert (forall ((x63 Int)) (=> (and (X1  x63) (<=  x63 0)) false)))
(assert (forall ((tmp64 Int)(x62 Int)) (=> (and (=  tmp64 (-  0 x62)) (X3  x62)) (X4  tmp64))))
(assert (forall ((x42 Int)(x61 Int)) (=> (and (X3  x42) (X4  x61)) (X2  x61))))
(assert (forall ((tmp65 Int)(x60 Int)) (=> (and (=  tmp65 x60) (X9  x60)) (X30  x60 tmp65))))
(assert (forall ((x59 Int)(z28 Int)) (=> (and (X9  z28) (X12  x59)) (X8  x59))))
(assert (forall ((x58 Int)(z28 Int)) (=> (and (X9  z28) (X11  x58)) (X7  x58))))
(assert (forall ((t39 Int)(x57 Int)(z28 Int)) (=> (and (and (X9  z28) (X11  t39)) (X6  x57)) (X10  x57))))
(assert (forall ((x56 Int)(z7 Int)) (=> (X30  x56 z7) (X11  x56))))
(assert (forall ((t39 Int)(x55 Int)(z7 Int)) (=> (and (X30  t39 z7) (X10  x55)) (X29  x55 z7))))
(assert (forall ((x54 Int)(z7 Int)) (=> (X29  x54 z7) (X11  x54))))
(assert (forall ((t39 Int)(x53 Int)(z7 Int)) (=> (and (X29  t39 z7) (X10  x53)) (X12  x53))))
(assert (forall ((tmp66 Int)(x52 Int)) (=> (and (=  tmp66 x52) (and (X0  x52) (>  x52 0))) (X28  x52 tmp66))))
(assert (forall ((n4 Int)(x51 Int)) (=> (X28  x51 n4) (X26  x51 n4))))
(assert (forall ((n4 Int)(x50 Int)(z28 Int)) (=> (and (X28  z28 n4) (X27  x50 n4)) (X1  x50))))
(assert (forall ((n4 Int)(x49 Int)) (=> (X26  x49 n4) (X9  x49))))
(assert (forall ((n4 Int)(x48 Int)(z28 Int)) (=> (and (X26  z28 n4) (X8  x48)) (X27  x48 n4))))
(assert (forall ((n4 Int)(x47 Int)(z28 Int)) (=> (and (X26  z28 n4) (X7  x47)) (X3  x47))))
(assert (forall ((n4 Int)(t24 Int)(x46 Int)(z28 Int)) (=> (and (and (X26  z28 n4) (X7  t24)) (X2  x46)) (X6  x46))))
(check-sat)
(get-proof)

Output

unsat
(error "
  could not reconstruct entry points
  while writing unsat proof
")

Version

Hoice 1.8.1(I manually built hoice. Rust version: rustc 1.39.0 (4560ea788 2019-11-04)
z3 4.8.8

To avoid this bug

When I replaced background z3 4.8.8 for z3 4.8.4, it worked well.

unsat
(
  (X0 1)
)

Parse error for sorts beginning with Int

When I pass the following datatype declarations to hoice 1.9.0,

(declare-datatypes ((IntBox 0)) ((par () (
  (IntBox-0 (IntBox-0.0 Int))))))
(declare-datatypes ((Expr 0)) ((par () (
  (Expr-0 (Expr-0.0 IntBox) (Expr-0.1 IntBox))
  (Expr-1 (Expr-1.0 IntBox))))))

I get the following error message.

(error "
  unknown sort `Box` on selector `Expr-0.0` of constructor `Expr-0` at [6:24]:
    |
  6 |   (Expr-0 (Expr-0.0 IntBox) (Expr-0.1 IntBox))
    |                        ^
  while parsing the declaration for this datatype at [5:22]:
    |
  5 | (declare-datatypes ((Expr 0)) ((par () (
    |                      ^
")

I tried similar examples and noticed that hoice fails at parsing sorts beginning with Int.

parse error on CHCs with ground assertions

I get the following parse error when CHC have ground assertions:
expected forall or negated exists

example
commit

Parsing or

I am confused with the way HoIce parses "or".
For the following input, HoIce seems to reject the 2nd and 5th clauses but accepts the other.
(The comments indicates error messages generated by HoIce.)

(set-logic HORN)
(declare-fun X () Bool)
(declare-fun Y () Bool)
(declare-fun Z () Bool)

(assert (forall () (=> (or X Y) Z)))
(assert (forall () (=> (or X (and Y Z)) Z)))  ;; ill-formed horn clause (or, 2)
(assert (forall () (=> (and X (or Y Z)) Z)))
(assert (forall () (=> (and (or X Y) (or X Z)) Z)))
(assert (forall () (=> (and (or X Y) (or X Z) (or X Y)) Z))) ;; error during clause conversion
(check-sat)

Parse error on result of `get-model` for Z3

For this input,

(set-logic HORN)
(declare-fun inv-f (Int Int Int Int Int Int Int Int Int) Bool)
(assert (forall ((A Int)
         (B Int)
         (C Int)
         (D Int)
         (E Int)
         (F Int)
         (G Int)
         (H Int)
         (I Int))
  (=> (and (= I E) (= H B) (= E 4) (= B 0) (inv-f I H G F E D C B A))
         false)
    ))
(assert (forall ((A Int)
         (B Int)
         (C Int)
         (D Int)
         (E Int)
         (F Int)
         (G Int)
         (H Int)
         (I Int))
  (=> (and (<= F 2) (<= C 2) (>= F 0) (>= C 0) (= I F) (= H C))
         (inv-f I H G F E D C B A))
    ))
(assert (forall ((A Int)
         (B Int)
         (C Int)
         (D Int)
         (E Int)
         (F Int)
         (G Int)
         (H Int)
         (I Int)
         (J Int)
         (K Int)
         (L Int)
         (M Int)
         (N Int)
         (O Int)
         (P Int)
         (Q Int)
         (R Int))
  (let ((a!1 (or (not (= O G))
                    (not (= M Q))
                    (not (= L R))
                    (not (= L (+ M 2)))
                    (not (= J P))
                    (not (= I H))
                    (not (= I (+ J 2))))))
     (let ((a!2 (and (or (not (= Q R))
                         (not (= P H))
                         (not (= O G))
                         (not (= M R))
                         (not (= M Q))
                         (not (= J P))
                         (not (= J H)))
                     a!1)))
       (=> (and (inv-f Q P O N M L K J I) (not a!2)) (inv-f R H G F E D C B A))))
    ))
 
(check-sat)
(exit)

the output is a parse error message :

(error "
  parse error: expected `model` on `(define-fun v_4 () Int
      4)`
")

Do you happen to know the reason of the parse error?

By the way, the version of Z3 I used is 4.8.10, and the version of hoice is 1.8.3.

bug?

Hoice (1.9.0, with Z3 4.8.11) returns "unsat", but I think the correct answer is actually "sat".

(declare-fun q (Int Int) Bool)
(assert (forall ((c Int) (d Int))
  (=> (and (q c d) (> c 0) (> d 0))
      false)))
(assert (forall ((c Int) (d Int))
  (=> (< c 0) (q c d))))
(assert (forall ((c Int) (d Int))
  (=> (< d 0) (q c d))))
(assert (forall ((c Int) (d Int) (m Int) (n Int))
  (=> (and (> m n) (>= n (+ (* c m) d))
           (q c (- d 1)) (q (- c 1) d))
      (q c d))))

(check-sat)
(get-model)

Z3 returns the following model

(
  (define-fun q ((x!0 Int) (x!1 Int)) Bool
    (or (<= x!0 0) (<= x!1 0)))
)

hoice get stuck during preprocessing

hoice (v1.10.0) gets stuck during pre-processing for the following input:

(set-logic HORN)
(declare-datatypes ((IList 0)) (((insert (head Int) (tail IList)) (nil))))

(declare-fun X (Int IList ) Bool)
(declare-fun size (IList Int) Bool)

(assert (forall ((x Int)) (size nil 0)))
(assert (forall ((x Int) (ls IList) (n Int))
	(=> (size ls n) (size (insert x ls) (+ n 1)))))
	
(assert (forall ((x Int)(ls IList)) (=> (and (X  x  ls) (<=  x 0 )) false)))
(assert (forall ((x Int)(ls IList)) (=> (and (X  x  ls) (=  (head ls) 0 ) ) (X  (- x 1) (tail ls)))))
(assert (forall ((m Int) (n Int) (ls IList)) (=> (and (size ls n) (>=  m n)) (X  m  ls))))
(check-sat)

Log:

koba@koba-PC:~$ hoice --version
hoice 1.10.0

koba@koba-PC:~$ hoice -v -v -v foo.smt2
; Running top pre-processing
; running simplify
;   simplifying clause #4 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
;   simplifying clause #3 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
;   simplifying clause #2 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
;   simplifying clause #1 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
;   simplifying clause #0 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
;     redundancy check...
;     split disj...
;     done
; simplify: did nothing
; running arg_reduce
;     rm_args (2)
;     to keep {
;       X: v_0 v_1
;       size: v_0 v_1
;     }
; arg_reduce: did nothing
; running one_rhs
; one_rhs: did nothing
; running one_lhs
; one_lhs: did nothing
; running fun_preds
;   working on size
;     working on clause #0
;     working on clause #1
;     checking 6 invariants...
;       not an invariant: (>= (* (- 1) v_1) 1)
;       confirmed invariant: (>= v_1 0)
;       not an invariant: (not (= v_1 0))
;       not an invariant: (= v_1 0)
;       not an invariant: (>= v_1 1)
;       not an invariant: (>= (* (- 1) v_1) 0)
;     discovered 1 invariant(s)
;     all branches are exclusive
;     checking they're exhaustive
;     branches are exhaustive
;   simplifying clause #2 (terms_changed: true)
;     propagation...
;     pruning...
;     trivial?
  C-c C-c

It seems

self.is_clause_trivial(clause)

on line 439 of instance/pre_instance.rs gets stuck.

Too slow to parse

HoIce cannot efficiently parse the attached file.

slow_parse.zip

Error for unsat proof

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 |[email protected]| ( Int (Array Int Int) Int ) Bool)
(declare-fun |[email protected]| ( ) Bool)
(declare-fun |main@_11| ( Int Int (Array Int Int) Int ) Bool)
(declare-fun |[email protected]| ( (Array Int Int) ) Bool)

(assert
  (forall ( (A (Array Int Int)) ) 
    (=>
      (and
        true
      )
      ([email protected] 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
        ([email protected] 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)))
      )
      ([email protected] Y Z A1)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) (D Bool) (E Int) (F (Array Int Int)) (G Int) ) 
    (=>
      (and
        ([email protected] E F G)
        (and (or (not D) (and C D))
     (or (not C) (and A C))
     (= D true)
     (or (not C) (not A) B))
      )
      ([email protected] E F G)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Int) (D Bool) (E Int) (F Int) (G (Array Int Int)) (H Int) ) 
    (=>
      (and
        ([email protected] 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)))
      )
      [email protected]
    )
  )
)
(assert
  (forall ( (CHC_COMP_UNUSED Bool) ) 
    (=>
      (and
        [email protected]
        true
      )
      false
    )
  )
)

(check-sat)
(exit)

Another bug?

(error "
asked for unsat proof while learning data is not unsat
")
for:

(set-logic HORN)
(declare-fun Entry_ (Int) Bool)
(declare-fun F (Int) Bool)
(declare-fun G (Int Int Int Int) Bool)
(declare-fun |F'| (Int Int Int) Bool)
(declare-fun P!!1 (Int Int Int Int) Bool)
(assert (forall ((A Int)) (=> (F A) (Entry_ A))))
(assert (forall ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int))
(let ((a!1 (and (G C B A F)
(= A (- E 1))
(= B (- D 1))
(or (>= E 0) (not (= F 100))))))
(=> a!1 (G C D E F)))))
(assert (forall ((A Int) (B Int) (C Int) (D Int)) (=> (<= B 0) (G A B C D))))
(assert (forall ((A Int) (B Int) (C Int) (D Int) (E Int) (F Int) (G Int) (H Int))
(=> (and (P!!1 H G F E)
(|F'| D G C)
(|F'| B G A)
(= A (+ H 1))
(= B (- F 1))
(= C (- H 1))
(= D (- F 1)))
(|F'| F G H))))
(assert (forall ((A Int) (B Int) (C Int) (D Int)) (=> (F D) (P!!1 D C B A))))
(assert (forall ((A Int) (B Int) (C Int) (D Int))
(let ((a!1 (>= A C)))
(=> (and (G B A C D) a!1 ) (P!!1 D C B A)))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (<= A 0) (|F'| A B C))))
(assert (forall ((A Int) (B Int))
(let ((a!1 (and (|F'| A B 0) (>= A 100))))
(=> a!1 (F B)))))

(assert (forall ((X0 Int)) (not (Entry_ X0))))
(check-sat)
(exit)

How SVCOMP benchmark programs are converting to Ocamal programs or to Horn cluases

Hi,

I would like to know how you are converting SVCOMP benchmark programs in either C or JAVA to OCamal or Horn Clauses. I understand Hoice can take only Horn Clauses. and r_type can be used for converting OCamal to Horn Clauses.

Thanks
Ezudheen

cargo test fails in rust 1.64.0

The output for cargo test

$ cargo test
    Finished test [unoptimized + debuginfo] target(s) in 0.25s
     Running unittests src/hoice.rs (target/debug/deps/hoice-8c0ebc4b1caf9f8b)

running 40 tests
test dtyp::dtyp_write_dec ... ok
...(omitted)....
test src/common/macros.rs - common::macros::try_val (line 382) ... FAILED
...(omitted)...
---- src/common/macros.rs - common::macros::try_val (line 382) stdout ----
error: cannot find macro `try_val` in this scope
  --> src/common/macros.rs:390:7
   |
11 |   Ok( try_val!{ bool val } )
   |       ^^^^^^^

error: cannot find macro `try_val` in this scope
 --> src/common/macros.rs:387:7
  |
8 |   Ok( try_val!{ int val } )
  |       ^^^^^^^

error[E0412]: cannot find type `Res` in this scope
 --> src/common/macros.rs:386:21
  |
7 | fn int(val: Val) -> Res<Val> {
  |                     ^^^ not found in this scope
  |
help: consider importing this type alias
  |
2 | use hoice::errors::Res;
  |

error[E0412]: cannot find type `Res` in this scope
  --> src/common/macros.rs:389:22
   |
10 | fn bool(val: Val) -> Res<Val> {
   |                      ^^^ not found in this scope
   |
help: consider importing this type alias
   |
2  | use hoice::errors::Res;
   |

error[E0603]: type alias `Val` is private
  --> src/common/macros.rs:383:18
   |
4  | use hoice::term::Val ;
   |                  ^^^ private type alias
   |
note: the type alias `Val` is defined here
  --> /home/katsura/github.com/hopv/hoice/src/term.rs:60:5
   |
60 | use crate::common::*;
   |     ^^^^^^^^^^^^^^^^

error: unused import: `hoice::errors`
 --> src/common/macros.rs:384:5
  |
5 | use hoice::errors ;
  |     ^^^^^^^^^^^^^
  |
note: the lint level is defined here
 --> src/common/macros.rs:380:9
  |
1 | #![deny(warnings)]
  |         ^^^^^^^^
  = note: `#[deny(unused_imports)]` implied by `#[deny(warnings)]`

error: aborting due to 6 previous errors

Some errors have detailed explanations: E0412, E0603.
For more information about an error, try `rustc --explain E0412`.
Couldn't compile the test.

failures:
    src/common/macros.rs - common::macros::try_val (line 382)

test result: FAILED. 215 passed; 1 failed; 0 ignored; 0 measured; 0 filtered out; finished in 53.01s

It looks like the doctest for common::macros::try_val is actually broken, but in the past stable cargo did not complain about it because it ignored that test. In fact, if I switch my toolchain version to 1.60.0, then cargo test successfully passes since it seems to ignore this broken test (well, presumably, cargo in 1.60.0 was broken with some reason 🤷 ).

I'm not sure about the implementation of hoice, so I cannot fix this problem myself, but the test should be fixed so that CI won't complain anymore about this.

Bug?

For the following input:

---

(set-logic HORN)
(declare-fun X (Int Int) Bool)
(declare-fun F (Int Int) Bool)
(declare-fun Entry_ () Bool)
(assert (forall ((A Int) (B Int) (C Int) (D Int))
(let ((a!1 (and (F B A) (= A (* 2 C D)) (= B (+ (* C C) (* D D))))))
(=> a!1 (X C D)))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (and (X B A) (= A (- C 1))) (X B C))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (and (X B A) (= A (+ C 1))) (X B C))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (and (X A C) (= A (- B 1))) (X B C))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (and (X A C) (= A (+ B 1))) (X B C))))
(assert (forall ((A Int) (B Int) (C Int) (D Int))
(=> (and (F B A) (= A (- D 1)) (= B (- C 1)) (> D 0)) (F C D))))
(assert (forall ((A Int) (B Int)) (=> (< A 0) (F A B))))
(assert (forall () (=> (X 0 0) Entry_)))

(assert (forall () (not Entry_)))
(check-sat)
(exit)

---

Hoice produces the following error:
(error "
solver error: "line 454 column 57: unknown function/constant F"
")

Mysterious bug around conditional branching

The following CHC system is satisfiable (which CHC solvers like Spacer rightly judge), but hoice (ver.1.8.3) judges it unsatisfiable.
Probably this bug is related to conditional branching.

(set-logic HORN)

(declare-fun main (Bool) Bool)
(declare-fun go (Int Int Bool) Bool)
(declare-fun go2 (Int Bool) Bool)

(assert (forall ((r Bool)) (=> (go 0 0 r) (main r))))
(assert (forall ((r Bool)) (=> (go 1 1 r) (main r))))
(assert (forall ((n Int)) (go n 0 true)))
(assert (forall ((n Int) (m Int) (r Bool))
  (=> (and (distinct m 0) (go2 n r)) (go n m r))))
(assert (forall ((? Int)) (go2 1 true)))
(assert (forall ((n Int)) (=> (distinct n 1) (go2 n false))))

(assert (forall ((r Bool)) (=> (main r) r)))
(check-sat)

Failed to parse model from solver.

For this input:

(set-logic HORN)

(declare-fun str_invariant
             (Int
              Int
              Bool
              Bool
              Bool
              Bool
              Bool
              Int
              Int
              Int
              Int
              Bool
              Bool
              Bool
              Bool
              Bool)
             Bool)
(assert (forall ((A Bool)
         (B Bool)
         (C Bool)
         (D Bool)
         (E Bool)
         (F Int)
         (G Int)
         (H Int)
         (I Int)
         (J Bool)
         (K Bool)
         (L Bool)
         (M Bool)
         (N Bool)
         (O Int)
         (P Int))
  (=> (and (str_invariant P O N M L K J I H G F E D C B A) (not (= K true)))
         false)
    ))
(assert (forall ((A Bool)
         (B Bool)
         (C Bool)
         (D Bool)
         (E Bool)
         (F Int)
         (G Int)
         (H Int)
         (I Int)
         (J Bool)
         (K Bool)
         (L Bool)
         (M Bool)
         (N Bool)
         (O Int)
         (P Int))
  (let ((a!1 (= E (and (>= I 1) (>= H 1) (=> (>= G I) M) (=> (>= F H) L)))))
       (=> (and (= J true)
                (= C true)
                (= B true)
                (= A true)
                (= K true)
                (= I P)
                (= H O)
                (= G 0)
                (= F 0)
                a!1
                (= D E))
           (str_invariant P O N M L K J I H G F E D C B A)))
    ))
(assert (forall ((A Int)
         (B Int)
         (C Bool)
         (D Bool)
         (E Bool)
         (F Bool)
         (G Bool)
         (H Bool)
         (I Bool)
         (J Bool)
         (K Bool)
         (L Bool)
         (M Int)
         (N Int)
         (O Int)
         (P Int)
         (Q Bool)
         (R Bool)
         (S Bool)
         (T Bool)
         (U Int)
         (V Bool)
         (W Int)
         (X Int)
         (Y Bool)
         (Z Bool)
         (A1 Bool)
         (B1 Bool)
         (C1 Bool)
         (D1 Int)
         (E1 Int)
         (F1 Int))
  (let ((a!1 (= E1 (ite V (+ (- N 1) 1) 0)))
           (a!2 (= D1 (ite T (+ (- M 1) 1) 0)))
           (a!3 (= C1 (and (>= B 1) (>= A 1) (=> (>= E1 B) F) (=> (>= D1 A) E))))
           (a!4 (=> B1 (=> (>= E1 (+ B A)) E))))
       (=> (and (str_invariant X W V T S R Q P O N M L K I H G)
                (not (= A1 true))
                (not (= Z true))
                (not (= Y true))
                (not (= C true))
                a!1
                a!2
                a!3
                (= B1 (or C1 K))
                (= D a!4)
                (= B P)
                (= A O))
           (str_invariant F1 U J F E D C B A E1 D1 C1 B1 A1 Z Y)))
    ))


(check-sat)
(exit)

the output is :

(error "
  failed to parse model from solver
")

I have updated hoice to this version : https://github.com/AdrienChampion/hoice/tree/warnings_and_rsmt2_update,
and the version of Z3 I used is 4.8.10.

a fresh declaration was already defined under Z3 4.8.9

Input

(set-logic HORN)
(declare-fun pred7 (Int ) Bool)
(declare-fun pred5 (Int Int ) Bool)
(declare-fun pred14 (Int ) Bool)
(declare-fun pred12 (Int Int ) Bool)
(declare-fun pred21 (Int ) Bool)
(declare-fun pred19 (Int Int ) Bool)
(declare-fun pred26 (Int Int ) Bool)
(declare-fun pred32 (Int Int ) Bool)
(declare-fun pred37 (Int ) Bool)
(assert (forall ((n_4 Int) (var40 Int) ) (=> (and (and true (pred7 n_4)) (= var40 (- n_4 1))) (pred5 n_4 var40))))
(assert (forall ((n_6 Int) (var41 Int) ) (=> (and (and (and true (pred14 n_6)) (= n_6 0)) (= var41 1)) (pred12 n_6 var41))))
(assert (forall ((n_6 Int) (var42 Int) ) (=> (and (and (and true (pred14 n_6)) (not (= n_6 0))) (= var42 n_6)) (pred7 var42))))
(assert (forall ((n_6 Int) (var45 Int) ) (=> (and (and (and true (pred14 n_6)) (not (= n_6 0))) (pred26 n_6 var45)) (pred5 n_6 var45))))
(assert (forall ((n_6 Int) (var44 Int) ) (=> (and (and (and true (pred14 n_6)) (not (= n_6 0))) (pred5 n_6 var44)) (pred26 n_6 var44))))
(assert (forall ((n_6 Int) (m_9 Int) (var46 Int) ) (=> (and (and (and (and true (pred14 n_6)) (not (= n_6 0))) (pred26 n_6 m_9)) (= var46 m_9)) (pred21 var46))))
(assert (forall ((n_6 Int) (m_9 Int) (var49 Int) ) (=> (and (and (and (and true (pred14 n_6)) (not (= n_6 0))) (pred26 n_6 m_9)) (pred12 n_6 var49)) (pred19 m_9 var49))))
(assert (forall ((n_6 Int) (m_9 Int) (var48 Int) ) (=> (and (and (and (and true (pred14 n_6)) (not (= n_6 0))) (pred26 n_6 m_9)) (pred19 m_9 var48)) (pred12 n_6 var48))))
(assert (forall ((n_10 Int) (var50 Int) ) (=> (and (and (and true (pred21 n_10)) (= n_10 0)) (= var50 0)) (pred19 n_10 var50))))
(assert (forall ((n_10 Int) (var51 Int) ) (=> (and (and (and true (pred21 n_10)) (not (= n_10 0))) (= var51 n_10)) (pred7 var51))))
(assert (forall ((n_10 Int) (var54 Int) ) (=> (and (and (and true (pred21 n_10)) (not (= n_10 0))) (pred32 n_10 var54)) (pred5 n_10 var54))))
(assert (forall ((n_10 Int) (var53 Int) ) (=> (and (and (and true (pred21 n_10)) (not (= n_10 0))) (pred5 n_10 var53)) (pred32 n_10 var53))))
(assert (forall ((n_10 Int) (m_13 Int) (var55 Int) ) (=> (and (and (and (and true (pred21 n_10)) (not (= n_10 0))) (pred32 n_10 m_13)) (= var55 m_13)) (pred14 var55))))
(assert (forall ((n_10 Int) (m_13 Int) (var58 Int) ) (=> (and (and (and (and true (pred21 n_10)) (not (= n_10 0))) (pred32 n_10 m_13)) (pred19 n_10 var58)) (pred12 m_13 var58))))
(assert (forall ((n_10 Int) (m_13 Int) (var57 Int) ) (=> (and (and (and (and true (pred21 n_10)) (not (= n_10 0))) (pred32 n_10 m_13)) (pred12 m_13 var57)) (pred19 n_10 var57))))
(assert (forall ((n_15 Int) (var59 Int) ) (=> (and (and (and true true) (>= n_15 0)) (= var59 n_15)) (pred14 var59))))
(assert (forall ((n_15 Int) (var62 Int) ) (=> (and (and (and true true) (>= n_15 0)) (pred37 var62)) (pred12 n_15 var62))))
(assert (forall ((n_15 Int) (var61 Int) ) (=> (and (and (and true true) (>= n_15 0)) (pred12 n_15 var61)) (pred37 var61))))
(assert (forall ((x Int) (y Int)) (=> (and (pred26 x y) (pred32 y x)) false)))
(check-sat)
(get-model)

Output

(error "
  solver error: "line 25 column 31: invalid named expression, declaration already defined with this name p_2 0"
  from ice learner
")
unknown
(error "
  no model available
")

The input does not include p_2, but the error occurred.

Version

• hoice 1.8.3
• cargo 1.43.0
• Z3 version 4.8.9

To avoid this bug

When I replaced Z3 4.8.9 with Z3 4.8.4, I avoided this bug.

Stack overflow

Hoice is aborted with:

thread 'main' has overflowed its stack
fatal runtime error: stack overflow

for the input below.
Does HoIce properly support integer arrays?

(declare-fun |[email protected]| ( ) Bool)
(declare-fun |[email protected]| ( (Array Int Int) (Array Int Int) Int Int Int ) Bool)
(declare-fun |[email protected]| ( Int Int Int (Array Int Int) ) Bool)
(declare-fun |main@entry| ( (Array Int Int) ) Bool)
(declare-fun |sum| ( Bool Bool Bool (Array Int Int) (Array Int Int) Int Int Int ) Bool)
(declare-fun |sum@_sm| ( (Array Int Int) Int Int ) Bool)
(declare-fun |main@_4| ( Int Int (Array Int Int) Int Int ) Bool)

(assert
  (forall ( (A (Array Int Int)) (B (Array Int Int)) (C Int) (D Int) (E Int) (v_5 Bool) (v_6 Bool) (v_7 Bool) ) 
    (=>
      (and
        (and true (= v_5 true) (= v_6 true) (= v_7 true))
      )
      (sum v_5 v_6 v_7 A B C D E)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) (B (Array Int Int)) (C Int) (D Int) (E Int) (v_5 Bool) (v_6 Bool) (v_7 Bool) ) 
    (=>
      (and
        (and true (= v_5 false) (= v_6 true) (= v_7 true))
      )
      (sum v_5 v_6 v_7 A B C D E)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) (B (Array Int Int)) (C Int) (D Int) (E Int) (v_5 Bool) (v_6 Bool) (v_7 Bool) ) 
    (=>
      (and
        (and true (= v_5 false) (= v_6 false) (= v_7 false))
      )
      (sum v_5 v_6 v_7 A B C D E)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) (B (Array Int Int)) (C Int) (D Int) (E Int) (v_5 Bool) (v_6 Bool) (v_7 Bool) ) 
    (=>
      (and
        ([email protected] A B E D C)
        (and (= v_5 true) (= v_6 false) (= v_7 false))
      )
      (sum v_5 v_6 v_7 A B C D E)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) (B Int) (C Int) ) 
    (=>
      (and
        true
      )
      (sum@_sm A B C)
    )
  )
)
(assert
  (forall ( (A Int) (B Int) (C Int) (D Bool) (E Bool) (F Bool) (G Bool) (H Int) (I Bool) (J Int) (K Bool) (L Int) (M Int) (N (Array Int Int)) (O Int) (P (Array Int Int)) (Q Bool) (R Int) (S (Array Int Int)) (T Bool) (U Int) (V Bool) (W Bool) (X (Array Int Int)) (Y (Array Int Int)) (Z Int) (A1 Int) (B1 Int) (v_28 Bool) (v_29 Bool) ) 
    (=>
      (and
        (sum@_sm X A1 B1)
        (sum T v_28 v_29 X N A B C)
        (and (= v_28 false)
     (= v_29 false)
     (or (not G) (not E) (not D))
     (or (not Q) K I)
     (or (not (<= B 0)) (<= A1 0) (not T))
     (or (not T) (not F) (not D))
     (or (not V) (and V T) (and V Q))
     (or (not V) (not Q) (= P X))
     (or (not V) (not Q) (= Y P))
     (or (not V) (not Q) (= R M))
     (or (not V) (not Q) (= Z R))
     (or (not V) (not T) (= S N))
     (or (not V) (not T) (= Y S))
     (or (not V) (not T) (= U O))
     (or (not V) (not T) (= Z U))
     (or (not D) (= F (= B1 1)))
     (or (not D) (= H (select X A1)))
     (or (not D) (and E D))
     (or (not I) (= J H))
     (or (not I) (= M J))
     (or (not I) D)
     (or (not I) F)
     (or (not K) (= L 0))
     (or (not K) (= M L))
     (or (not K) E)
     (or (not K) G)
     (or (not T) (= A (+ (- 1) B1)))
     (or (not T) (= B (+ 4 A1)))
     (or (not T) (= O (+ C H)))
     (or (not T) (and T D))
     (or (not W) (and W V))
     (= W true)
     (not (= (<= 1 B1) G)))
      )
      ([email protected] X Y Z A1 B1)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) ) 
    (=>
      (and
        true
      )
      (main@entry A)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) (B Bool) (C Bool) (D Int) (E Int) (F Bool) (G Bool) (H Int) (I Int) (J Int) (K (Array Int Int)) ) 
    (=>
      (and
        (main@entry A)
        (and (not (= (<= 0 E) C))
     (= B (= J 999))
     (= D (* (- 1) E))
     (= I (ite C D E))
     (or (not G) (and G F))
     (= B true)
     (= G true)
     (= K A))
      )
      ([email protected] H I J K)
    )
  )
)
(assert
  (forall ( (A Bool) (B Bool) (C Bool) (D Bool) (E Int) (F Int) (G Int) (H (Array Int Int)) ) 
    (=>
      (and
        ([email protected] E F G H)
        (and (or (not C) (and A C))
     (or (not D) (and D C))
     (= D true)
     (or (not C) B (not A)))
      )
      ([email protected] E F G H)
    )
  )
)
(assert
  (forall ( (A Bool) (B (Array Int Int)) (C (Array Int Int)) (D Bool) (E Int) (F Bool) (G Int) (H Int) (I (Array Int Int)) (J Int) (K Int) ) 
    (=>
      (and
        ([email protected] G J K B)
        (and (or (not F) (= I C) (not D))
     (or (not F) (= E 0) (not D))
     (or (not F) (= H E) (not D))
     (or (not F) (not A) (not D))
     (or (not F) (and D F))
     (= F true)
     (or (not F) (= C B) (not D)))
      )
      (main@_4 G H I J K)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) (B Int) (C Int) (D Bool) (E (Array Int Int)) (F Int) (G (Array Int Int)) (H Bool) (I Int) (J Bool) (K Int) (L Int) (M (Array Int Int)) (N Int) (O Int) ) 
    (=>
      (and
        (main@_4 K C A N O)
        (and (not (= (<= O C) D))
     (= F (+ 1 C))
     (= B (+ K (* 4 C)))
     (not (<= K 0))
     (or (not J) (= G E) (not H))
     (or (not J) (= M G) (not H))
     (or (not J) (= I F) (not H))
     (or (not J) (= L I) (not H))
     (or (not J) D (not H))
     (or (<= K 0) (not (<= B 0)))
     (or (not J) (and H J))
     (= J true)
     (= E (store A B N)))
      )
      (main@_4 K L M N O)
    )
  )
)
(assert
  (forall ( (A (Array Int Int)) (B Int) (C Int) (D Int) (E Int) (F Int) (G Bool) (H Bool) (I Int) (J (Array Int Int)) (K (Array Int Int)) (L Int) (M Int) (N Bool) (O Bool) (P Bool) (v_16 Bool) (v_17 Bool) (v_18 Int) ) 
    (=>
      (and
        (main@_4 I E A C F)
        (sum O v_16 v_17 J K v_18 L M)
        (let ((a!1 (or (not O) (not (= (<= M (- 1)) N)))))
  (and (= v_16 false)
       (= v_17 false)
       (= 1000 v_18)
       (not (= (<= F E) H))
       (= B (+ I (* 4 E)))
       (= D (+ 1 E))
       (not (<= I 0))
       (or (not O) (not (<= L 0)) (<= I 0))
       (or (not H) (not O) (not G))
       (or (<= I 0) (not (<= B 0)))
       a!1
       (or (not O) (= L I))
       (or (not O) (and G O))
       (or (not O) (not N))
       (or (not P) (and P O))
       (= P true)
       (= J (store A B C))))
      )
      [email protected]
    )
  )
)
(assert
  (forall ( (CHC_COMP_UNUSED Bool) ) 
    (=>
      (and
        [email protected]
        true
      )
      false
    )
  )
)

(check-sat)
(exit)

bug: "invalid named expression"?

I got an error message:

(error "
  solver error: "line 45 column 0: invalid named expression, declaration already defined with this name q"
")

for the following input.

(set-logic HORN)
(declare-fun q (Int Int) Bool)
(assert (forall ((c Int) (d Int))
  (=> (and (q c d) (> c 0) (> d 0))
      false)))
(assert (forall ((c Int) (d Int))
  (=> (< d 0) (q c d))))
(assert (forall ((c Int) (d Int))
  (=> (q (- c 1) d)
      (q c d))))

(check-sat)
(get-model)

What's going on here?

Bug?

Running
hoice foo.smt2 --timeout 1
produces the error:
(error "
Broken pipe (os error 32)
from ice learner
")

for the following input foo.smt2:

(set-logic HORN)
(declare-fun X (Int Int) Bool)
(declare-fun F (Int Int) Bool)
(declare-fun Entry_ () Bool)
(assert (forall ((A Int) (B Int) (C Int) (D Int))
(let ((a!1 (and (F B A) (= A (* 2 C D)) (= B (+ (* C C) (* D D))))))
(=> a!1 (X C D)))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (and (X B A) (= A (- C 1))) (X B C))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (and (X B A) (= A (+ C 1))) (X B C))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (and (X A C) (= A (- B 1))) (X B C))))
(assert (forall ((A Int) (B Int) (C Int)) (=> (and (X A C) (= A (+ B 1))) (X B C))))
(assert (forall ((A Int) (B Int) (C Int) (D Int))
(=> (and (F B A) (= A (- D 1)) (= B (- C 1)) (> D 0)) (F C D))))
(assert (forall ((A Int) (B Int)) (=> (< A 0) (F A B))))
(assert (forall () (=> (X 0 0) Entry_)))

(assert (forall () (not Entry_)))
(check-sat)
(exit)

Release-built hoice sometimes crashes while learning on macOS Monterey

Input

(set-logic HORN)

(declare-fun
  main@_6
  ( Int Int Int ) Bool
)
(declare-fun
  [email protected]
  ( Int Int Int Int ) Bool
)
(declare-fun
  [email protected]
  ( Int Int ) Bool
)

(assert 
  (forall
    ( (A Int) (C Int) (I Int) (J Int) )
    (=>
      (and
        (>= (+ C (* (- 1) J)) 0) (>= (+ I (* (- 1) A)) 1)
        ([email protected] C A I J)
      )
      ([email protected] (+ C (- 1)) (+ A 1) I J)
    )
  )
)

(assert 
  (forall
    ( (H Int) (I Int) )
    (=>
      (and
        true
        true
      )
      (main@_6 0 H I)
    )
  )
)

(assert 
  (forall
    ( (A Int) (B Int) (D Int) )
    (=>
      (and
        (not (= D 0))
        ([email protected] A B)
      )
      ([email protected] (+ A 1) (+ B 1))
    )
  )
)

(assert 
  (forall
    ( (B Int) (C Int) (L Int) (M Int) )
    (=>
      (and
        (not (= B 0))
        (main@_6 C L M)
      )
      (main@_6 (+ C 1) L M)
    )
  )
)

(assert 
  (forall
    ( (B Int) (C Int) (D Int) )
    (=>
      (and
        (or (>= (+ C (* (- 1) B)) 1) (>= (+ D (* (- 1) C)) 0))
        (main@_6 C B D)
      )
      ([email protected] 0 0 (- 1) 1)
    )
  )
)

(assert 
  (forall
    ( (A Int) (B Int) (C Int) (H Int) )
    (=>
      (and
        (or (>= (+ B (* (- 1) A)) 1) (>= (+ C (* (- 1) B)) 0)) (not (= H 0))
        (main@_6 B A C)
      )
      ([email protected] 0 0)
    )
  )
)
(assert 
  (forall
    ( (A Int) (C Int) (D Int) (G Int) )
    (=>
      (and
        (>= (+ G (* (- 1) A)) 2) (>= (+ D (* (- 1) C)) 1)
        ([email protected] (+ A 1) C D G)
      )
      false
    )
  )
)
(assert 
  (forall
    ( (B Int) (I Int) )
    (=>
      (and
        true
        ([email protected] I B)
      )
      ([email protected] (+ B 1) 0 I 1)
    )
  )
)
(check-sat)

Output (sometimes)

hoice(62406,0x70000f03c000) malloc: *** error for object 0x600002c34bb0: pointer being freed was not allocated
hoice(62406,0x70000f03c000) malloc: *** set a breakpoint in malloc_error_break to debug
fish: Job 1, './target/release/hoice --log_...' terminated by signal SIGABRT (Abort)

Version

macOS Monterey 12.2.1
hoice 1.8.1 (manually built(1c9a5d110 2021-01-29)
z3 4.8.13
rustc 1.60.0

This error doesn't happen on Debian 11, z3 4.8.13, rustc 1.57.0

Stack Trace

hoice(63567,0x70000b73a000) malloc: *** error for object 0x600003500000: pointer being freed was not allocated
hoice(63567,0x70000b73a000) malloc: *** set a breakpoint in malloc_error_break to debug
  thread #2, name = 'ice', stop reason = signal SIGABRT
    frame #0: 0x00007ff805dd0112 libsystem_kernel.dylib`__pthread_kill + 10
    frame #1: 0x00007ff805e06214 libsystem_pthread.dylib`pthread_kill + 263
    frame #2: 0x00007ff805d52d10 libsystem_c.dylib`abort + 123
    frame #3: 0x00007ff805c303e2 libsystem_malloc.dylib`malloc_vreport + 548
    frame #4: 0x00007ff805c335ed libsystem_malloc.dylib`malloc_report + 151
    frame #5: 0x00000001002754b7 hoice`hoice::data::Data::destroy::hb59ed86746733263 + 2887
    frame #6: 0x00000001000c77a3 hoice`hoice::learning::ice::IceLearner::learn::h4fa19c30151517de + 1283
    frame #7: 0x00000001000c6238 hoice`hoice::learning::ice::IceLearner::run::h847aee6c547ef342 + 1800
    frame #8: 0x00000001000c43a4 hoice`hoice::learning::ice::Launcher::launch::h86dedf9dfc6a0166 + 436
    frame #9: 0x0000000100336752 hoice`std::sys_common::backtrace::__rust_begin_short_backtrace::hf1caa9859d2433f7 + 162
    frame #10: 0x000000010019faa2 hoice`core::ops::function::FnOnce::call_once$u7b$$u7b$vtable.shim$u7d$$u7d$::h3fd6720881912218 + 178
    frame #11: 0x00000001003de767 hoice`std::sys::unix::thread::Thread::new::thread_start::h9b70539161da4eaf [inlined] _$LT$alloc..boxed..Box$LT$F$C$A$GT$$u20$as$u20$core..ops..function..FnOnce$LT$Args$GT$$GT$::call_once::h76ed59d8775c95eb at boxed.rs:1853:9 [opt]
    frame #12: 0x00000001003de761 hoice`std::sys::unix::thread::Thread::new::thread_start::h9b70539161da4eaf [inlined] _$LT$alloc..boxed..Box$LT$F$C$A$GT$$u20$as$u20$core..ops..function..FnOnce$LT$Args$GT$$GT$::call_once::h9a39ecfa1322b383 at boxed.rs:1853:9 [opt]
    frame #13: 0x00000001003de75a hoice`std::sys::unix::thread::Thread::new::thread_start::h9b70539161da4eaf at thread.rs:108:17 [opt]
    frame #14: 0x00007ff805e064f4 libsystem_pthread.dylib`_pthread_start + 125
    frame #15: 0x00007ff805e0200f libsystem_pthread.dylib`thread_start + 15
libsystem_kernel.dylib`__pthread_kill:
    0x7ff805dd0108 <+0>:  movl   $0x2000148, %eax          ; imm = 0x2000148 
    0x7ff805dd010d <+5>:  movq   %rcx, %r10
    0x7ff805dd0110 <+8>:  syscall 
->  0x7ff805dd0112 <+10>: jae    0x7ff805dd011c            ; <+20>
    0x7ff805dd0114 <+12>: movq   %rax, %rdi
    0x7ff805dd0117 <+15>: jmp    0x7ff805dca2f1            ; cerror_nocancel
    0x7ff805dd011c <+20>: retq   
    0x7ff805dd011d <+21>: nop    
    0x7ff805dd011e <+22>: nop    
    0x7ff805dd011f <+23>: nop
     rax = 0x0000000000000000
     rdx = 0x0000000000000000
     rbx = 0x000070000b73a000
     rbp = 0x000070000b737ab0
     rsp = 0x000070000b737a88

Mysterious bug on lists and pairs

The following SMT2 code is not accepted by HoIce, probably by a bug.

I tried the following code on HoIce. (Sorry for this noisy and messy bug report!)

(set-logic HORN)

(declare-datatypes ((Mut 1)) ((par (T) ((mut (cur T) (ret T))))))
(declare-datatypes ((List 1)) ((par (T) (nil (insert (head T) (tail (List T)))))))

(declare-fun inck (Int (Mut (List Int))) Bool)
(assert (forall ((k Int))
  (=> true
    (inck k (mut nil nil)))
))
(assert (forall ((k Int) (x Int) (xs (List Int)) (xs! (List Int)))
  (=> (inck k (mut xs xs!))
    (inck k (mut (insert x xs) (insert (+ x k) xs!))))
))

(declare-fun length ((List Int) Int) Bool)
(assert (forall ((dummy Int))
  (=> true (length nil 0))
))
(assert (forall ((n Int) (x Int) (xs (List Int)))
  (=> (length xs n) (length (insert x xs) (+ 1 n)))
))

(declare-fun sum ((List Int) Int) Bool)
(assert (forall ((dummy Int))
  (=> true (sum nil 0))
))
(assert (forall ((n Int) (x Int) (xs (List Int)))
  (=> (sum xs n) (sum (insert x xs) (+ x n)))
))

(assert (forall ((n Int) (l Int) (r Int) (k Int) (xs (List Int)) (xs! (List Int)))
  (=> (and (sum xs n) (length xs l) (inck k (mut xs xs!)) (sum xs! r))
    (= r (+ n (* k l))))
))

(check-sat)
(get-model)

Passing the code above to HoIce under z3 4.7.1, I will unexpectedly get the following error.

(error "
  solver error: "line 30 column 54: unknown function/constant mut"
")

Interestingly, when I just swap the two arguments of inck, I will get unsat.

unsat
(error "
  no model available
")

However, the expected answer is sat.

Fix/Enhance Error-Handling

Hoice's error-handling is based on error-chain and has several issues as far as Hoice is concerned.

The main problem is that error-chain erases errors, i.e. rsmt2's errors become dyn std::error::Error and it is not possible to know what the error is anymore.
(One very bad way is to check their description, but it's way too ugly to consider.)

This becomes bad because in some cases (pre-processing is the main example), it is convenient for hoice to encode the fact that a/some clause(s) are unsat/unknown as an Error. This leads to either contrived error-handling or bad behavior, such as #36.

I think hoice should have its own custom error-handling approach, which is actually not that hard to do. It could even be (mostly) compatible with error-chain's API. This custom approach should allow to

• chain errors in a similar fashion to error-chain,
• access the actual root (original) error without any type erasure.