Bug #5453
[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]
Ошибка плавающая, т.е. пока не удалось так подобрать аргументы программы, чтобы сделать её воспроизводимой.
History
Updated by Sergey Smolov about 6 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 about 6 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 about 6 years ago
- Status changed from Feedback to Resolved
My test says "ok" for this solution.
Updated by Andrei Tatarnikov about 6 years ago
- Status changed from Verified to Closed
- % Done changed from 0 to 100
- Published in build set to 141226