Actions
Bug #5453
closed[arrays] Unexpected solver output: " (INSTQUEUE ((as const (Array Int Int)) 0))"
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]
Ошибка плавающая, т.е. пока не удалось так подобрать аргументы программы, чтобы сделать её воспроизводимой.
Actions