Skip to content

Commit 6dc492d

Browse files
committed
Update regression test quoting for Windows compatibility
The " double quote works when used with cbmc directly on the Windows `cmd.exe` command line, but not when used in combination with `test.pl`. So this commit swaps to usage of ' single quotes instead, which does work with `test.pl` on Windows.
1 parent b22d2e7 commit 6dc492d

File tree

4 files changed

+4
-4
lines changed

4 files changed

+4
-4
lines changed

regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE winbug
22
control_flow.c
3-
--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
3+
--incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
44
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
55
Sending command to SMT2 solver - \(set-option :produce-models true\)
66
Sending command to SMT2 solver - \(set-logic QF_UFBV\)

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE winbug
22
test.c
3-
--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
3+
--incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
44
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
55
Sending command to SMT2 solver - \(set-option :produce-models true\)
66
Sending command to SMT2 solver - \(set-logic QF_UFBV\)

regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE winbug
22
trace.c
3-
--incremental-smt2-solver "z3 --smt2 -in" --trace
3+
--incremental-smt2-solver 'z3 --smt2 -in' --trace
44
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
55
Assert of inequality to 4\.: FAILURE
66
Assert of inequality to 2\.: FAILURE

regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE winbug
22
valid_unsat.c
3-
--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
3+
--incremental-smt2-solver 'z3 --smt2 -in' --verbosity 10
44
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
55
Sending command to SMT2 solver - \(check-sat\)
66
Solver response - unsat

0 commit comments

Comments
 (0)