Project

General

Profile

Actions
Copy link

Bug #7557

closed

ConstCastTestCase: java.lang.AssertionError: Calculator failed to substitute result

Added by Sergey Smolov over 8 years ago. Updated over 8 years ago.

Status:
Closed
Priority:
High
Assignee:
Artem Kotsynyak
Category:
-
Target version:
0.4
Start date:
09/07/2016
Due date:
% Done:

0%

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

Description

Probable bug in calculator, because ConstCastTestCase falls upon calling it.

Calculator failed to substitute result:
(AND (EQ (POWER y 3) z))
-> (LET () (AND (EQ (POWER y 3) z)))
-> (AND (EQ (POWER y 3) z))
-> (AND (EQ (POWER y 3) z))
java.lang.AssertionError: Calculator failed to substitute result:
(AND (EQ (POWER y 3) z))
-> (LET () (AND (EQ (POWER y 3) z)))
-> (AND (EQ (POWER y 3) z))
-> (AND (EQ (POWER y 3) z))
    at org.junit.Assert.fail(Assert.java:88)
    at org.junit.Assert.assertTrue(Assert.java:41)
    at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.checkResult(GenericSolverTestBase.java:210)
    at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.solveAndCheckResult(GenericSolverTestBase.java:174)
    at ru.ispras.fortress.solver.constraint.GenericSolverTestBase.runSolverTests(GenericSolverTestBase.java:110)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
Actions
Copy link
 #1

Updated by Artem Kotsynyak over 8 years ago

  • Status changed from New to Closed

Reject. CVC4 have no support for 'power' in SMT2 parser since it is not standard operation.

Actions
Copy link

Also available in: Atom PDF