Retrascope » Retrascope Test Suite

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)