mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
dc8087713d
* Activate FPA theory as default Activating FPA as default introduce a tiny time regression (about 1%) but we prove more goals on both `ae-format` and `why3-gallery`. Fix issue #917
9 lines
160 B
Plaintext
9 lines
160 B
Plaintext
|
|
unknown
|
|
(
|
|
(define-fun x () Pair
|
|
(pair (store (as @a3 (Array Int S)) 0 s)
|
|
(store (as @a3 (Array Int S)) 0 s)))
|
|
(define-fun s () S (as @a2 S))
|
|
)
|