Project

General

Profile

Actions
Copy link

Bug #9562

closed

ru.ispras.retrascope.engine.hldd.printer.smv.usedef.MemStageUseDefSmvPrinterTestCase: model checker crashes without errors in *.smvlog

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

Status:
Closed
Priority:
Normal
Assignee:
Mikhail Lebedev
Category:
Engine
Target version:
1.0
Start date:
03/25/2019
Due date:
% Done:

0%

Estimated time:
Detected in build:
master
Platform:
Published in build:
1.1.1-beta-190722

Description

ru.ispras.retrascope.basis.exception.RetrascopeException: Model checker exited with error! See 'MEM_stage.smvlog' for details:
Last 50 lines of the log file:

    at ru.ispras.retrascope.engine.smv.launcher.SmvModelCheckerLauncher.analyzeResult(SmvModelCheckerLauncher.java:162)
    at ru.ispras.retrascope.engine.smv.launcher.SmvModelCheckerLauncher.runChecker(SmvModelCheckerLauncher.java:149)
    at ru.ispras.retrascope.engine.smv.launcher.SmvModelCheckerLauncher.start(SmvModelCheckerLauncher.java:137)
    at ru.ispras.retrascope.basis.Engine.start(Engine.java:332)
    at ru.ispras.retrascope.basis.ToolChain.start(ToolChain.java:111)
    at ru.ispras.retrascope.basis.Engine.start(Engine.java:332)
    at ru.ispras.retrascope.Retrascope$ToolRun.start(Retrascope.java:222)
    at ru.ispras.retrascope.Retrascope.main(Retrascope.java:463)
    at ru.ispras.retrascope.Retrascope.main(Retrascope.java:380)
    at ru.ispras.retrascope.util.ToolTest.runTest(ToolTest.java:113)
    at ru.ispras.retrascope.engine.hldd.printer.smv.usedef.UseDefSmvPrinterVerilogTest.runTest(UseDefSmvPrinterVerilogTest.java:43)

The "MEM_stage.smvlog" file is:

*** This is nuXmv 1.1.1 (compiled on Wed Jun  1 10:18:42 2016)
*** Copyright (c) 2014-2016, Fondazione Bruno Kessler

*** For more information on nuXmv see https://nuxmv.fbk.eu
*** or email to <nuxmv@list.fbk.eu>.
*** Please report bugs at https://nuxmv.fbk.eu/bugs
*** (click on "Login Anonymously" to access)
*** Alternatively write to <nuxmv@list.fbk.eu>.

*** This version of nuXmv is linked to NuSMV 2.6.0.
*** For more information on NuSMV see <http://nusmv.fbk.eu>
*** or email to <nusmv-users@list.fbk.eu>.
*** Copyright (C) 2010-2014, Fondazione Bruno Kessler

*** This version of nuXmv is linked to the CUDD library version 2.4.1
*** Copyright (c) 1995-2004, Regents of the University of Colorado

*** This version of nuXmv is linked to the MiniSat SAT solver. 
*** See http://minisat.se/MiniSat.html
*** Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
*** Copyright (c) 2007-2010, Niklas Sorensson

*** This version of nuXmv is linked to MathSAT
*** Copyright (C) 2009-2016 by Fondazione Bruno Kessler
*** Copyright (C) 2009-2016 by University of Trento
*** See http://mathsat.fbk.eu

Actions
Copy link
 #1

Updated by Sergey Smolov over 5 years ago

  • Status changed from New to Closed
  • Published in build set to 1.1.1-beta-190722

It seems that model checker crashes for some internal reason. At least, now we have error code. The ticket is closed.

Actions
Copy link

Also available in: Atom PDF