mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
61b5b3e41b
* Use a separated counter for abstract value Use a separated counter in `Models` to produce fresh names for abstract values in models. This fix is temporary as we plan to refactor the model generation in another PR. A better design consists in producing fresh names while computing the model. * Increase the counter * Promote tests I also add another tests to check if the counter increases properly.
13 lines
308 B
Plaintext
13 lines
308 B
Plaintext
(set-logic ALL)
|
|
(set-option :produce-models true)
|
|
(declare-const x Int)
|
|
(declare-const y Int)
|
|
(declare-const a1 (Array Int Int))
|
|
(declare-const a2 (Array Int Int))
|
|
(assert (= (select a1 x) x))
|
|
(assert (= (store a1 x y) a1))
|
|
(assert (= (select a2 x) x))
|
|
(assert (= (store a2 x y) a1))
|
|
(check-sat)
|
|
(get-model)
|