tests/models/array/array1.models.expected


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))
)
Use a separated counter for abstract value (#835) * 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. 2023-09-25 12:34:21 +02:00
			`unknown`
			`(`
			`(define-fun x () Int 0)`
			`(define-fun y () Int 0)`
cleanup: Use proper namespacing for names (#1028) 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. 2024-01-22 10:50:12 +01:00			`(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))`
Use a separated counter for abstract value (#835) * 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. 2023-09-25 12:34:21 +02:00			`)`