Project

General

Profile

Bug #5453

[arrays] Unexpected solver output: " (INSTQUEUE ((as const (Array Int Int)) 0))"

Added by Sergey Smolov about 5 years ago. Updated about 5 years ago.

Status:
Closed
Priority:
High
Assignee:
Artem Kotsynyak
Category:
-
Target version:
0.3
Start date:
11/27/2014
Due date:
% Done:

100%

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

Description

При анализе HDL-описаний инструментом Retrascope иногда возникает ошибка со следующим логом:

[log]

java.lang.AssertionError: Unexpected solver output: " (INSTQUEUE ((as const (Array Int Int)) 0))"
at ru.ispras.fortress.solver.engine.z3.Z3TextSolver.solve(Z3TextSolver.java:136)
at ru.ispras.fortress.solver.constraint.ConstraintUtils.solve(ConstraintUtils.java:69)
at ru.ispras.fortress.expression.ExprUtils.isSAT(ExprUtils.java:303)
at ru.ispras.fortress.expression.ExprUtils.areCompatible(ExprUtils.java:288)

[/log]

Ошибка плавающая, т.е. пока не удалось так подобрать аргументы программы, чтобы сделать её воспроизводимой.

History

#1

Updated by Sergey Smolov about 5 years ago

  • Subject changed from Unexpected solver output: " (INSTQUEUE ((as const (Array Int Int)) 0))" to [arrays] Unexpected solver output: " (INSTQUEUE ((as const (Array Int Int)) 0))"
#2

Updated by Artem Kotsynyak about 5 years ago

  • Status changed from New to Feedback

Done preliminary in r710, const arrays being interpreted as empty arrays. The only way I've come to reproduce "as const" Z3 output is illegal SMT with broken parentheses balance that Z3 tries to fix.

#3

Updated by Sergey Smolov about 5 years ago

  • Status changed from Feedback to Resolved

My test says "ok" for this solution.

#4

Updated by Sergey Smolov about 5 years ago

  • Status changed from Resolved to Verified
#5

Updated by Andrei Tatarnikov about 5 years ago

  • Status changed from Verified to Closed
  • % Done changed from 0 to 100
  • Published in build set to 141226

Also available in: Atom PDF