Project

General

Profile

Actions

Bug #5401

closed

error at ru/ispras/fortress/solver/constraint/ArrayTestCase.java

Added by Sergey Smolov over 9 years ago. Updated about 9 years ago.

Status:
Closed
Priority:
Normal
Assignee:
Andrei Tatarnikov
Category:
-
Target version:
Start date:
10/30/2014
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Platform:
Published in build:
141226

Description

Приведенный в тесте ru/ispras/fortress/solver/constraint/ArrayTestCase.java пример на языке SMT-LIB не выполняется решателем Z3:

[log]

Z3: ERROR: unexpected character sat ((a (_ as-array k!1))) ((v (_ as-array k!0))) (model (define-fun v () (Array Int Int) (_ as-array k!0)) (define-fun a () (Array Int Int) (_ as-array k!1)) (define-fun k!0 ((x!1 Int)) Int 0) (define-fun k!1 ((x!1 Int)) Int (ite (= x!1 37) 37 0)) )

[/log]

Код на SMT-LIB:

[code]

(define-sort ARRAY_TYPE () (Array Int Int))
(declare-fun a () ARRAY_TYPE)
(declare-fun v () ARRAY_TYPE)
(assert (= a (store v 37 37)))
(assert (= a '((37 37))))
(check-sat)
(get-value (a))
(get-value (v))
(get-model)
(exit)

[/code]

Actions

Also available in: Atom PDF