Project

General

Profile

Actions
Copy link

Bug #9309

closed

ru.ispras.retrascope.engine.smv.testbench.sample.vcegar.VcegarPiBusAssertSmvTestbenchTestCase:line 2 column 34: invalid declaration, builtin symbol select

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

Status:
Closed
Priority:
Normal
Assignee:
Sergey Smolov
Category:
Retrascope
Start date:
10/05/2018
Due date:
% Done:

100%

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

Description

java.lang.IllegalArgumentException: Constraint contains errors: (AND (AND (AND (EQ cebjjgfhd_PHASE 000011) (EQ select 1)) true) (AND (EQ pi_state 00)) (AND (AND (BVUGE cebjjgfhd_PHASE 000000) (BVULE cebjjgfhd_PHASE 101001)))); errors=[line 2 column 34: invalid declaration, builtin symbol select, line 9 column 12: select takes at least two arguments, line 20 column 2: select takes at least two arguments, (declare-const pi_state (_ BitVec 2))
(declare-const select (_ BitVec 1))
(declare-const cebjjgfhd_PHASE (_ BitVec 6))
(assert 
   (and
     (and
       (and
         (= cebjjgfhd_PHASE #b000011)
         (= select #b1))
       true)
     (and
       (= pi_state #b00))
     (and
       (and
         (bvuge cebjjgfhd_PHASE #b000000)
         (bvule cebjjgfhd_PHASE #b101001)))))
(check-sat)
(get-value (
  pi_state
  select
  cebjjgfhd_PHASE
  ))
(get-model)
(exit)
]
    at ru.ispras.retrascope.util.SatSolver.isSat(SatSolver.java:158)
    at ru.ispras.retrascope.util.SolverUtils.isSat(SolverUtils.java:42)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createTransitionsFrom(CgaaEfsmTransformer.java:574)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createTransitions(CgaaEfsmTransformer.java:549)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.createEfsm(CgaaEfsmTransformer.java:518)
    at ru.ispras.retrascope.engine.cgaa.transformer.efsm.CgaaEfsmTransformer.getOutput(CgaaEfsmTransformer.java:426)
    at ru.ispras.retrascope.engine.basis.ModelWalkerEngine.start(ModelWalkerEngine.java:84)
    at ru.ispras.retrascope.basis.Engine.start(Engine.java:223)
    at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:111)
    at ru.ispras.retrascope.basis.Engine.start(Engine.java:223)
    at ru.ispras.retrascope.Retrascope$ToolRun.start(Retrascope.java:215)
    at ru.ispras.retrascope.Retrascope.main(Retrascope.java:456)
    at ru.ispras.retrascope.Retrascope.main(Retrascope.java:373)
    at ru.ispras.retrascope.util.ToolTest.runTest(ToolTest.java:93)
    at ru.ispras.retrascope.basis.SingleTest.runTest(SingleTest.java:91)
    at ru.ispras.retrascope.engine.smv.testbench.sample.vcegar.VcegarAssertSmvTestbenchSingleTest.runTest(VcegarAssertSmvTestbenchSingleTest.java:38)

Related issues 1 (0 open — 1 closed)

Related to Retrascope - Task #9310: substitute SMT-LIB variables those names are equal to builtin commandsClosedSergey Smolov10/05/2018

Actions
Actions
Copy link

Also available in: Atom PDF