Bug #5453
closed[arrays] Unexpected solver output: " (INSTQUEUE ((as const (Array Int Int)) 0))"
100%
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]
Ошибка плавающая, т.е. пока не удалось так подобрать аргументы программы, чтобы сделать её воспроизводимой.
Updated by Sergey Smolov almost 10 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))"
Updated by Artem Kotsynyak almost 10 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.
Updated by Sergey Smolov almost 10 years ago
- Status changed from Feedback to Resolved
My test says "ok" for this solution.
Updated by Sergey Smolov almost 10 years ago
- Status changed from Resolved to Verified
Updated by Andrei Tatarnikov almost 10 years ago
- Status changed from Verified to Closed
- % Done changed from 0 to 100
- Published in build set to 141226