[BUG] Assumptions are (silently) ignored

[lemmy]

----- MODULE Bar ----
CONSTANT
    \* @type: Bool;
    P

\* Should "catch" P = FALSE
ASSUME P = TRUE

VARIABLE
   \* @type: Bool;
    x

Init ==
    x = P

Next ==
    UNCHANGED x

Inv ==
    x = TRUE
=====

CONSTANT
    P = FALSE
INIT
    Init
NEXT 
    Next
INVARIANT 
    Inv

markus@avocado:~$ apalache check --config=Bar.cfg Bar
# Tool home: /home/markus/src/TLA/_community/apalache
# Package:   /home/markus/src/TLA/_community/apalache/mod-distribution/target/apalache-pkg-0.15.9-SNAPSHOT-full.jar
# JVM args:  -Xmx4096m -DTLA-Library=/home/markus/src/TLA/_community/apalache/src/tla
#
# APALACHE version 0.15.9-SNAPSHOT build v0.15.8-3-g6a26844
#
# WARNING: This tool is in the experimental stage.
#          Please report bugs at: [https://github.com/informalsystems/apalache/issues]
# 
# Usage statistics is ON. Thank you!
# If you have changed your mind, disable the statistics with config --enable-stats=false.

Checker options: filename=Bar, init=, next=, inv=                 I@15:54:36.199
Tuning:                                                           I@15:54:36.650
PASS #0: SanyParser                                               I@15:54:36.652
Parsing file /home/markus/src/TLA/_specs/models/tutorials/BlockingQueueTLA/Bar.tla
PASS #1: TypeCheckerSnowcat                                       I@15:54:37.310
 > Running Snowcat .::.                                           I@15:54:37.311
 > Your types are great!                                          I@15:54:37.450
 > All expressions are typed                                      I@15:54:37.450
PASS #2: ConfigurationPass                                        I@15:54:37.481
  > Bar.cfg: Loading TLC configuration                            I@15:54:37.485
  > Using the init predicate Init from the TLC config             I@15:54:37.562
  > Using the next predicate Next from the TLC config             I@15:54:37.562
  > Bar.cfg: found INVARIANTS: Inv                                I@15:54:37.562
  > Set the initialization predicate to Init                      I@15:54:37.564
  > Set the transition predicate to Next                          I@15:54:37.565
  > Set an invariant to Inv                                       I@15:54:37.566
  > Replaced CONSTANT P with FALSE                                I@15:54:37.569
PASS #3: DesugarerPass                                            I@15:54:37.606
  > Desugaring...                                                 I@15:54:37.607
PASS #4: UnrollPass                                               I@15:54:37.639
  > Unroller                                                      I@15:54:37.656
PASS #5: PrimingPass                                              I@15:54:37.685
  > Introducing InitPrimed for Init'                              I@15:54:37.692
PASS #6: CoverAnalysisPass                                        I@15:54:37.722
PASS #7: InlinePass                                               I@15:54:37.724
  > InlinerOfUserOper                                             I@15:54:37.728
  > LetInExpander                                                 I@15:54:37.729
  > FoldOperLetinizer                                             I@15:54:37.730
  > InlinerOfUserOper                                             I@15:54:37.731
Leaving only relevant operators: CInitPrimed, Init, InitPrimed, Inv, Next I@15:54:37.735
PASS #8: VCGen                                                    I@15:54:37.764
  > Producing verification conditions from the invariant Inv      I@15:54:37.765
  > VCGen produced 1 verification condition(s)                    I@15:54:37.777
PASS #9: PreprocessingPass                                        I@15:54:37.794
  > Before preprocessing: unique renaming                         I@15:54:37.794
 > Applying standard transformations:                             I@15:54:37.827
  > PrimePropagation                                              I@15:54:37.828
  > Desugarer                                                     I@15:54:37.843
  > UniqueRenamer                                                 I@15:54:37.858
  > Normalizer                                                    I@15:54:37.876
  > Keramelizer                                                   I@15:54:37.893
  > After preprocessing: UniqueRenamer                            I@15:54:37.907
PASS #10: TransitionFinderPass                                    I@15:54:37.923
  > Found 1 initializing transitions                              I@15:54:37.941
  > Found 1 transitions                                           I@15:54:37.942
  > No constant initializer                                       I@15:54:37.943
  > Applying unique renaming                                      I@15:54:37.944
PASS #11: OptimizationPass                                        I@15:54:37.956
 > Applying optimizations:                                        I@15:54:37.963
  > ConstSimplifier                                               I@15:54:37.964
  > ExprOptimizer                                                 I@15:54:37.966
  > ConstSimplifier                                               I@15:54:37.967
PASS #12: AnalysisPass                                            I@15:54:37.983
 > Marking skolemizable existentials and sets to be expanded...   I@15:54:37.988
  > SkolemizationMarker                                           I@15:54:37.989
  > ExpansionMarker                                               I@15:54:37.990
 > Running analyzers...                                           I@15:54:37.993
  > Introduced expression grades                                  I@15:54:38.007
  > Introduced 0 formula hints                                    I@15:54:38.007
PASS #13: PostTypeCheckerSnowcat                                  I@15:54:38.008
 > Running Snowcat .::.                                           I@15:54:38.008
 > Your types are great!                                          I@15:54:38.048
 > All expressions are typed                                      I@15:54:38.048
PASS #14: BoundedChecker                                          I@15:54:38.064
State 0: Checking 1 state invariants                              I@15:54:38.469
State 0: state invariant 0 violated. Check the counterexample in: counterexample1.tla, MC1.out, counterexample1.json E@15:54:38.502
Found 1 error(s)                                                  I@15:54:38.508
The outcome is: Error                                             I@15:54:38.509
Checker has found an error                                        I@15:54:38.509
It took me 0 days  0 hours  0 min  2 sec                          I@15:54:38.510
Total time: 2.387 sec                                             I@15:54:38.510
EXITCODE: ERROR (12)

[konnov]

Yep, the corresponding issue has a two-digit number: #69