Hari Govind V K

@leonardoalt this issue has been fixed in the latest commit #6820

I cannot reproduce the issue. For the instance [chc-LIA-Lin_325](https://github.com/chc-comp/chc-comp22-benchmarks/blob/main/LIA-Lin/chc-LIA-Lin_325.smt2.gz), when I run z3 without any parameters, I am getting the following model: ``` (define-fun main_1 ((x!0 Int) (x!1 Int) (x!2...

This model does satisfy the last CHC because it has the literal `(not (>= x!0 2))` .

Yes. It has to do with arrays indexed by other arrays and arrays indexed by finite types. The current MBP (and the earlier one) does not support this fragment. Its...

I have solved this problem in my local branch: https://github.com/hgvk94/z3/commit/aad4cac4b83378a45230d550c2fead0561c3aa94 I will merge it soon. However, even after the fix, global guidance doesn't solve this instance. It identifies the common...

Looks like your implementation works better than mine. Closing this PR.

Thanks. The example is simple enough. Looks like Spacer is getting stuck in the proof generation phase. Debugging this ...

[updates] Spacer is getting stuck in an SMT query made to the solver during proof generation. The query is [here](https://gist.github.com/hgvk94/2dbf172b9058cefdd9b093a471740920). This is commit that introduced this problem: https://github.com/Z3Prover/z3/commit/d0d434e4f1fc847abc38940f4a9e6d97bf1ec44a Debugging it...

The problem is when creating a model for an array expression. The `final_check` method attempts to merge all enodes that are not equal [here](https://github.com/Z3Prover/z3/blob/master/src/smt/theory_array_base.cpp#L565). However, with the new `is_unique_value` implementation...

Thanks for the detailed report. Taking a look ...