mirror of
https://github.com/AdaCore/alt-ergo.git
synced 2026-02-12 12:39:26 -08:00
e7fc6642e8
This introduces proper namespacing for variable names instead of relying on string prefixes. In order to disturb the ordering as little as possible, names are pre-mangled using their namespace (e.g. "x" in the `Internal` namespace is stored as ".!x") and further operations (hashing, comparison, etc.) are performed on the mangled names.
9 lines
213 B
Plaintext
9 lines
213 B
Plaintext
|
|
unknown
|
|
(
|
|
(define-fun x () Int 0)
|
|
(define-fun y () Int 0)
|
|
(define-fun a1 () (Array Int Int) (store (as @a4 (Array Int Int)) 0 0))
|
|
(define-fun a2 () (Array Int Int) (store (as @a5 (Array Int Int)) 0 0))
|
|
)
|