fresh_symbolic and abc

[msaaltink]

The C code is just your ffs.c example. The saw script:

l <- llvm_load_module "ffs.bc";
w <- fresh_symbolic "w" {| [32] |};
ffs <- llvm_symexec l "ffs_ref" [] [("word", w, 1)] [("return", 1)] false;
prove cvc4 {{ffs < 33}} ;
prove abc {{ffs < 33}} ;

The abc attempt fails with

evalTermF ExtCns unimplemented (w)

Abc is however perfectly happy to do the proof after an 'abstract_symbolic' step.

Incidentally, an attempt with mathsat fails with

Prover returned error: 
Failed to complete the call to MathSAT
Executable   : "/usr/local/bin/mathsat"
Options      : -input=smt2 -theory.fp.minmax_zero_mode=4
Exit code    : 1
Solver output: 
==============================================================================
ERROR: unknown option: theory.fp.minmax_zero_mode, value: 4, command-line: -theory.fp.minmax_zero_mode=4
==============================================================================
Giving up..

That mathsat option was added in Version 5.3.7 last July, and I'm a bit out of date - but why is that option even relevant here?