2010-10-26 15:49 Alessandro Mariotti <mariotti@fbk.eu>

	* src/cinit/cinitCmd.c, src/cinit/cinitData.c,
	  src/cinit/cinitInit.c, src/cinit/cinitMisc.c,
	  src/cinit/cinitVers.c: REFACTORING

	  Refactored package cinit in order to respect the coding rules.

2010-10-26 14:30 Alessandro Mariotti <mariotti@fbk.eu>

	* src/cinit/cinitCmd.c, src/cinit/cinitData.c,
	  src/cinit/cinitInit.c, src/cinit/cinitInt.h,
	  src/cinit/cinitMisc.c, src/cinit/cinitVers.c: REFACTORING

	  Renamed old functions with prefix "sm"

2010-10-26 13:31 Roberto Cavada <cavada@fbk.eu>

	* Makefile.am, configure.ac: BUG FIX This commit resolves these
	  issues:

	  1. configure.ac no longer uses deprecated parameters when
	  calling AM_INIT_AUTOMAKE

	  2. very old tar limited to 99 char in names is no longer used
	  (it was causing problems when generating html prog manual)

	  3. target distbin now strips the executables

2010-10-26 13:02 Roberto Cavada <cavada@fbk.eu>

	* helpers/extract_doc.in: BUG FIX Packages 'addons' and 'sm' were
	  renamed, but the doc extractor was not updated accordingly.

2010-10-25 14:03 Alessandro Mariotti <mariotti@fbk.eu>

	* src/cinit/cinitData.c: BUGFIX

	  Fixed mantis issue 2203: -bmc and -bmc_length options were
	  registered even if no SAT solver is given from the configuration
	  step.

2010-10-22 14:26 Marco Pensallorto <pensallorto@fbk.eu>

	* src/trace/TraceManager.c, test/traces/new/bug_6a.cmd,
	  test/traces/new/bug_6b.cmd: BUGFIX + TESTING

	  Fixed a small bug in symbols filtering. Thanks to AMa for
	  reporting it.

2010-10-22 13:48 Alessandro Mariotti <mariotti@fbk.eu>

	* src/compile/compileFlatten.c, src/fsm/sexp/Expr.c,
	  src/sexp/SexpInliner.c: BUGFIX

	  Fixed mantis issue 2194. All recursive uses of Expr_resolve have
	  been checked. Now real-time CTL operators have a special
	  treatment in order to preserve the range sub-expression.

2010-10-22 09:58 Marco Pensallorto <pensallorto@fbk.eu>

	* test/bug_2188, test/bug_2188/bug0.cmd, test/bug_2188/bug0.smv,
	  test/bug_2188/bug1.cmd, test/bug_2188/test.sh: TESTING

	  Added test case for issue #2188

2010-10-22 09:52 Marco Pensallorto <pensallorto@fbk.eu>

	* test/bug_1291, test/bug_1291/bug0.cmd, test/bug_1291/bug0.smv,
	  test/bug_1291/bug1.cmd, test/bug_1291/test.sh: TESTING

	  Added test case for issue #1291

2010-10-22 09:30 Marco Pensallorto <pensallorto@fbk.eu>

	* src/simulate/simulate.c: BUGFIX + MAINTENANCE

	  Refactored a function in simulate.c for easier readability and
	  maintainability. The constraints used into interactive
	  simulation are now properly type-checked before translating them
	  into BDDs.  This commit fixes issue #2188.

	  Also removed a couple of warnings due to incorrect typecasts.

2010-10-21 17:55 Andrea Micheli <amicheli@fbk.eu>

	* src/fsm/sexp/SexpFsm.c, src/fsm/sexp/SexpFsm_private.h: BUGFIX

	  Fixed bug #2078 (https://essvn.fbk.eu/bugs/view.php?id=2078).

	  * SexpFsm class now uses SexpInliner instead of its own inlining
	  routines.

	  * Inlining learning-phase now uses only invars for invars, invar
	  and init for init and invar and trans for trans to guarantee the
	  correctness of the inlined FSM.

	  * Old inlining routines and fields has been removed from SexpF
	  class.

2010-10-21 15:58 Alessandro Mariotti <mariotti@fbk.eu>

	* src/compile/symb_table/ResolveSymbol.c: BUGFIX

	  - Fixed seg.fault in the ModelSimplifierExpr class. The "Nil"
	  value for a process name was not correctly considered as "main"
	  constant value.

	  - Added an assertion to ResolveSymbol.c, where "name" parameter
	  of the ResolveSymbol_resolve function is expected to be non-NULL

2010-10-21 15:32 Andrea Micheli <amicheli@fbk.eu>

	* test/bug_2078, test/bug_2078/a.smv, test/bug_2078/t.cmd,
	  test/bug_2078/test.sh: NEW TESTCASE

	  Added testcase for bug #2078
	  (https://essvn.fbk.eu/bugs/view.php?id=2078).

2010-10-21 15:07 Marco Pensallorto <pensallorto@fbk.eu>

	* src/compile/compileCone.c: MAINTENANCE

	  Reverted a fix to compile cone on request of MR. I filed a
	  ticket regarding this issue (#2191) and added a warning.

2010-10-21 13:00 Alessandro Mariotti <mariotti@fbk.eu>

	* src/cinit/cinitInit.c, src/cinit/cinitInt.h, src/cmd/cmd.h,
	  src/cmd/cmdCmd.c, src/cmd/cmdFile.c, src/cmd/cmdInt.h,
	  src/cmd/cmdMisc.c, src/dd/dd.c, src/dd/dd.h, src/dd/ddCmd.c,
	  src/dd/ddInt.h, src/opt/OptsHandler.c, src/opt/OptsHandler.h,
	  src/opt/optCmd.c, src/opt/optInt.h,
	  src/trans/bdd/ClusterOptions.c: BUGFIX

	  - Fixed the echo command, which was not correctly printing
	  variables (e.g. echo $on_failure_script_quits outputs the value
	  of the variable instead of the string it self

	  - Removed obsolete variable cmdFlagTable and relative methods
	  and calls. This old system for holding variables values has been
	  replaced with the OptsHandler class.

2010-10-21 12:46 Marco Pensallorto <pensallorto@fbk.eu>

	* doc/user-man/inter.tex: DOCUMENTATION

	  Added reference to env vars traces_hiding_prefix and
	  traces_regexp in pick_state and simulate commands.

2010-10-21 12:17 Marco Pensallorto <pensallorto@fbk.eu>

	* src/compile/compileCone.c, src/compile/compileWrite.c,
	  src/compile/compileWriteUdg.c, src/opt/opt.h, src/opt/optCmd.c,
	  src/opt/optInt.h, src/simulate/simulateTransSet.c,
	  src/trace/TraceManager.c, src/trace/TraceManager.h,
	  src/trace/TraceOpt.c, src/trace/pkg_trace.c,
	  src/trace/pkg_trace.h, src/trace/plugins/TracePlugin.c: BUGFIX

	  This commit fixes issue 0001291: simulation commands do not
	  respect shell vars to filter variables. A bit of refactoring has
	  been done as described in the related Mantis ticket.

	  A few system variables has been renamed. Complete list follows:

	  counter_examples_hiding_prefix -> traces_hiding_prefix
	  counter_examples_show_re -> traces_regexp show_defines_in_traces
	  -> traces_show_defines trace_show_defines_with_next ->
	  traces_show_defines_with_next

2010-10-20 13:01 Alessandro Mariotti <mariotti@fbk.eu>

	* test/bug_2114, test/bug_2114/echo.cmd, test/bug_2114/test.sh:
	  TESTS

	  Added self test for bug 2114

2010-10-20 09:58 Alessandro Mariotti <mariotti@fbk.eu>

	* Makefile.am, configure.ac, src/Makefile.am, src/bmc/bmcDump.c,
	  src/bmc/bmcPkg.c, src/bmc/sbmc/sbmcPkg.c, src/cinit,
	  src/cinit/Makefile.am, src/cinit/cinit.h, src/cinit/cinitCmd.c,
	  src/cinit/cinitData.c, src/cinit/cinitDummyMac.c,
	  src/cinit/cinitInit.c, src/cinit/cinitInt.h,
	  src/cinit/cinitMisc.c, src/cinit/cinitVers.c, src/cinit/sm.h,
	  src/cinit/smCmd.c, src/cinit/smData.c, src/cinit/smDummyMac.c,
	  src/cinit/smInit.c, src/cinit/smInt.h, src/cinit/smMisc.c,
	  src/cinit/smVers.c, src/cmd/cmdFile.c, src/cmd/cmdInt.h,
	  src/cmd/cmdMisc.c, src/enc/bdd/BddEnc.c,
	  src/ltl/ltl2smv/ltl2smvMain.c, src/main.c, src/opt/optCmd.c,
	  src/opt/optInt.h, src/parser/parserUtil.c, src/sm,
	  src/utils/error.c: REFACTORING

	  Renamed package SM to CINIT. All function with Sm prefix have
	  been replaced with prefix CInit

	  All inclusions of sm/ files have been replaced with inclusions
	  of cinit/ files.

	  The system is tagged as follows:

	  before_sm_to_cinit_renaming_20102010
	  after_sm_to_cinit_renaming_20102010

2010-10-20 09:04 Alessandro Mariotti <mariotti@fbk.eu>

	* src/compile/FlatHierarchy.c, src/compile/FlatHierarchy.h,
	  src/fsm/FsmBuilder.c, src/fsm/sexp/SexpFsm.c,
	  src/fsm/sexp/SexpFsm_private.h: BUGFIX

	  Fixed mantis issue #2182 with the solution proposed in the bug
	  report.  Automatic test had been already added in the test/
	  directory.

2010-10-19 14:11 Alessandro Mariotti <mariotti@fbk.eu>

	* test/bug_2182, test/bug_2182/bug.smv, test/bug_2182/dump.smv,
	  test/bug_2182/read.cmd, test/bug_2182/test.sh,
	  test/bug_2182/write.cmd: TESTS\nAdded automatic test fot bug
	  2182\n

2010-10-12 09:13 Marco Pensallorto <pensallorto@fbk.eu>

	* src/trace/exec/BDDPartialTraceExecutor.c,
	  src/trace/exec/SATPartialTraceExecutor.c: BUGFIX

	  Fixed issue #2173. No error message was displayed under certain
	  circumstances in partial trace re-execution.

2010-10-12 09:11 Marco Pensallorto <pensallorto@fbk.eu>

	* test/bug_2173, test/bug_2173/1.smv, test/bug_2173/bug1.cmd,
	  test/bug_2173/bug2.cmd, test/bug_2173/bug3.cmd,
	  test/bug_2173/test.sh, test/bug_2173/trace.xml: TESTING

	  Added test case for issue #2173

2010-10-06 13:23 Alessandro Mariotti <mariotti@fbk.eu>

	* src/parser/psl/pslExpr.c, src/parser/psl/psl_grammar.y: FEATURE

	  Added support for expressions in array access in PSL. Some tests
	  have already been commited. This commit fixes mantis issue 1849

2010-10-06 10:08 Alessandro Mariotti <mariotti@fbk.eu>

	* test/bug_1849/bug.smv, test/bug_1849/bug1.smv,
	  test/bug_1849/bug2.smv, test/bug_1849/bug3.smv,
	  test/bug_1849/test.sh: TESTS

	  Added other automatic tests for the PSL extension of constant
	  expression in array indexes.

2010-10-05 15:32 Alessandro Mariotti <mariotti@fbk.eu>

	* src/compile/type_checking/checkers/CheckerCore.c: REFACTORING

	  Memory usage issue has been fixed: The type checker was using
	  SymbTable_get_define_flatten_body, which is known to use a lot
	  of resources in case of big models (with a lot of defines).

	  now the typechecker descends recursively using both the define
	  "unflattened" body and it's context, avoiding the flattening of
	  the defines.

	  This solves mantis issue 1925.

	  All related problems to this issue were fixed by using the
	  ResolveSymbol class, however, all regression tests have been
	  executed.

2010-10-05 13:22 Alessandro Mariotti <mariotti@fbk.eu>

	* src/compile/PredicateExtractor.c, test/bug_2161,
	  test/bug_2161/bug_count_0.smv, test/bug_2161/bug_count_1.smv,
	  test/bug_2161/test.sh: BUGFIX

	  Fixed bug 2161 that was making NuSMV result in a seg. fault.

	  pred_extract_process_recur returned objects were not correctly
	  handled, and this was causing a bad pointer read.

	  Fix has been double-checked with MR.

2010-10-05 12:14 Alessandro Mariotti <mariotti@fbk.eu>

	* src/mc/mcInvar.c: BUGFIX

	  Solved mantis issue 2145: Wrong results were reported when using
	  cached reachable states without layers information.

	  The issue has been fixed accordingly to mantis note 3940 (MR).
