fix in txExpr2z3Expr

[rasoolmaghareh]

We are planning to test this PR on our test programs. @ArpitaDutta please report the test results here. Thanks

[rasoolmaghareh]

I did test this PR on the tracerx-examples\basic folder and the results remain valid. There are some crashes that are related to data structures and array cases not supported yet. We have to deal with them separately.

[ArpitaDutta]

I have done testing of this PR on half of the programs from TracerX/tree/master/test/Smoke_Test using both the master branch and new-wpinterpolant branch (by making the required changes for new-wp).

Everything seems fine except for one program m34CTLAI-B3.c. For this program, the following error is obtained.

Could not attach to process. If your uid matches the uid of the target process, check the setting of /proc/sys/kernel/yama/ptrace_scope, or try again as the root user. For more details, see /etc/sysctl.d/10-ptrace.conf ptrace: Operation not permitted. No symbol table is loaded. Use the "file" command. The program is not being run. KLEE: WARNING: KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)

[rasoolmaghareh]

@ArpitaDutta can you please post the outputs for the m34CTLAI-B3.c. program here? Thanks

[ArpitaDutta]

Hi @rasoolmaghareh, Below is the output for m34CTLAI-B3.c. program.

Using Z3 solver backend
KLEE: WARNING: undefined reference to function: printf
KLEE: WARNING ONCE: calling external: printf(61476776)
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via INT

KLEE: ctrl-c detected, requesting interpreter to halt.
KLEE: WARNING: KLEE: WATCHDOG: time expired, attempting halt via gdb

Could not attach to process.  If your uid matches the uid of the target
process, check the setting of /proc/sys/kernel/yama/ptrace_scope, or try
again as the root user.  For more details, see /etc/sysctl.d/10-ptrace.conf
ptrace: Operation not permitted.
No symbol table is loaded.  Use the "file" command.
The program is not being run.
KLEE: WARNING: KLEE: WATCHDOG: kill(9)ing child (I tried to be nice)

---------------------------------------------------------------------------------------
|          Path          |  Instrs|  Time(s)|  ICov(%)|  BCov(%)|  ICount|  TSolver(%)|
---------------------------------------------------------------------------------------
|m34CTLAI-B3-3/klee-out-0|    8944|     6.62|     5.22|     4.80|   26329|        0.42|
---------------------------------------------------------------------------------------

[alvin21mfmlai]

Master-Branch (no modifications to Z3Simplification.cpp & with deletion)

Master-Branch (modifications to Z3Simplification.cpp & with deletion)

Persistent Memory-Branch (no modifications to Z3Simplification.cpp & with wp interpolant)

Persistent Memory-Branch (modifications to Z3Simplification.cpp & with wp interpolant)

Master-Branch (no modifications to Z3Simplification.cpp & with wp interpolant)

Master-Branch (modifications to Z3Simplification.cpp & with wp interpolant)