Assertion crash in FPA model construction (recent regression)

[nunoplopes]

Reproducer: file.zip

$ z3 smt.ematching=false file.smt2
ASSERTION VIOLATION
File: ../src/util/obj_hashtable.h
Line: 171
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

Trace:

#1  0x00007ffff667d74f in obj_map<smt::enode, app*>::find (k=<optimized out>,
    this=0x20) at ../src/ast/ast.h:505
#2  obj_map<smt::enode, app*>::operator[] (k=<optimized out>, this=0x20)
    at ../src/util/obj_hashtable.h:182
#3  smt::model_generator::get_value (this=this@entry=0xb5f628,
    n=n@entry=0xb84768) at ../src/smt/smt_model_generator.cpp:379
#4  0x00007ffff66849cf in smt::model_generator::mk_values (
    this=this@entry=0xb5f628) at ../src/smt/smt_model_generator.cpp:363
#5  0x00007ffff6684ca2 in smt::model_generator::mk_model (this=0xb5f628)
    at ../src/smt/smt_model_generator.cpp:500
#6  0x00007ffff66118f8 in smt::context::mk_proto_model (
    this=this@entry=0xb23968, r=r@entry=l_true)
    at ../src/smt/smt_context.cpp:4397

Git bisect says the regression was introduced in 77689ed

[wintersteiger]

Fixed, thanks for the report!

[wintersteiger]

Awesome, many thanks for the new fix!